<?xml version="1.0"?>
<doc>
    <assembly>
        <name>Microsoft.Z3</name>
    </assembly>
    <members>
        <member name="T:Microsoft.Z3.Expr">
            <summary>
            Expressions are terms.     
            </summary>
        </member>
        <member name="T:Microsoft.Z3.AST">
            <summary>
            The abstract syntax tree (AST) class. 
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Z3Object">
            <summary>
            Internal base class for interfacing with native Z3 objects.
            Should not be used externally.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Z3Object.Finalize">
            <summary>
            Finalizer.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.AST.op_Equality(Microsoft.Z3.AST,Microsoft.Z3.AST)">
            <summary>
            Comparison operator.
            </summary>
            <param name="a">An AST</param>
            <param name="b">An AST</param>
            <returns>True if <paramref name="a"/> and <paramref name="b"/> are from the same context 
            and represent the same sort; false otherwise.</returns>
        </member>
        <member name="M:Microsoft.Z3.AST.op_Inequality(Microsoft.Z3.AST,Microsoft.Z3.AST)">
            <summary>
            Comparison operator.
            </summary>
            <param name="a">An AST</param>
            <param name="b">An AST</param>
            <returns>True if <paramref name="a"/> and <paramref name="b"/> are not from the same context 
            or represent different sorts; false otherwise.</returns>
        </member>
        <member name="M:Microsoft.Z3.AST.Equals(System.Object)">
            <summary>
            Object comparison.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.AST.CompareTo(System.Object)">
            <summary>
            Object Comparison.
            </summary>
            <param name="other">Another AST</param>
            <returns>Negative if the object should be sorted before <paramref name="other"/>, positive if after else zero.</returns>
        </member>
        <member name="M:Microsoft.Z3.AST.GetHashCode">
            <summary>
            The AST's hash code.
            </summary>
            <returns>A hash code</returns>
        </member>
        <member name="M:Microsoft.Z3.AST.Translate(Microsoft.Z3.Context)">
            <summary>
            Translates (copies) the AST to the Context <paramref name="ctx"/>.
            </summary>
            <param name="ctx">A context</param>
            <returns>A copy of the AST which is associated with <paramref name="ctx"/></returns>
        </member>
        <member name="M:Microsoft.Z3.AST.ToString">
            <summary>
            A string representation of the AST.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.AST.SExpr">
            <summary>
            A string representation of the AST in s-expression notation.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.AST.Id">
            <summary>
            A unique identifier for the AST (unique among all ASTs).
            </summary>
        </member>
        <member name="P:Microsoft.Z3.AST.ASTKind">
            <summary>
            The kind of the AST.
            </summary>    
        </member>
        <member name="P:Microsoft.Z3.AST.IsExpr">
            <summary>
            Indicates whether the AST is an Expr
            </summary>
        </member>
        <member name="P:Microsoft.Z3.AST.IsVar">
            <summary>
            Indicates whether the AST is a BoundVariable
            </summary>
        </member>
        <member name="P:Microsoft.Z3.AST.IsQuantifier">
            <summary>
            Indicates whether the AST is a Quantifier
            </summary>
        </member>
        <member name="P:Microsoft.Z3.AST.IsSort">
            <summary>
            Indicates whether the AST is a Sort
            </summary>
        </member>
        <member name="P:Microsoft.Z3.AST.IsFuncDecl">
            <summary>
            Indicates whether the AST is a FunctionDeclaration
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Expr.Simplify(Microsoft.Z3.Params)">
            <summary>
            Returns a simplified version of the expression.
            </summary>
            <param name="p">A set of parameters to configure the simplifier</param>
            <seealso cref="M:Microsoft.Z3.Context.SimplifyHelp"/>
        </member>
        <member name="M:Microsoft.Z3.Expr.Update(Microsoft.Z3.Expr[])">
            <summary>
            Update the arguments of the expression using the arguments <paramref name="args"/>
            The number of new arguments should coincide with the current number of arguments.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Expr.Substitute(Microsoft.Z3.Expr[],Microsoft.Z3.Expr[])">
            <summary>
            Substitute every occurrence of <c>from[i]</c> in the expression with <c>to[i]</c>, for <c>i</c> smaller than <c>num_exprs</c>.
            </summary>
            <remarks>
            The result is the new expression. The arrays <c>from</c> and <c>to</c> must have size <c>num_exprs</c>.
            For every <c>i</c> smaller than <c>num_exprs</c>, we must have that 
            sort of <c>from[i]</c> must be equal to sort of <c>to[i]</c>.
            </remarks>    
        </member>
        <member name="M:Microsoft.Z3.Expr.Substitute(Microsoft.Z3.Expr,Microsoft.Z3.Expr)">
            <summary>
            Substitute every occurrence of <c>from</c> in the expression with <c>to</c>.
            </summary>
            <seealso cref="M:Microsoft.Z3.Expr.Substitute(Microsoft.Z3.Expr[],Microsoft.Z3.Expr[])"/>
        </member>
        <member name="M:Microsoft.Z3.Expr.SubstituteVars(Microsoft.Z3.Expr[])">
            <summary>
            Substitute the free variables in the expression with the expressions in <paramref name="to"/>
            </summary>
            <remarks>
            For every <c>i</c> smaller than <c>num_exprs</c>, the variable with de-Bruijn index <c>i</c> is replaced with term <c>to[i]</c>.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Expr.Translate(Microsoft.Z3.Context)">
            <summary>
            Translates (copies) the term to the Context <paramref name="ctx"/>.
            </summary>
            <param name="ctx">A context</param>
            <returns>A copy of the term which is associated with <paramref name="ctx"/></returns>
        </member>
        <member name="M:Microsoft.Z3.Expr.ToString">
            <summary>
            Returns a string representation of the expression.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Expr.#ctor(Microsoft.Z3.Context)">
            <summary> Constructor for Expr </summary>
        </member>
        <member name="M:Microsoft.Z3.Expr.#ctor(Microsoft.Z3.Context,System.IntPtr)">
            <summary> Constructor for Expr </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.FuncDecl">
            <summary>
            The function declaration of the function that is applied in this expression.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.BoolValue">
            <summary>
            Indicates whether the expression is the true or false expression
            or something else (Z3_L_UNDEF).
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.NumArgs">
            <summary>
            The number of arguments of the expression.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.Args">
            <summary>
            The arguments of the expression.
            </summary>        
        </member>
        <member name="P:Microsoft.Z3.Expr.IsNumeral">
            <summary>
            Indicates whether the term is a numeral
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsWellSorted">
            <summary>
            Indicates whether the term is well-sorted.
            </summary>
            <returns>True if the term is well-sorted, false otherwise.</returns>
        </member>
        <member name="P:Microsoft.Z3.Expr.Sort">
            <summary>
            The Sort of the term.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsConst">
            <summary>
            Indicates whether the term represents a constant.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsIntNum">
            <summary>
            Indicates whether the term is an integer numeral.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRatNum">
            <summary>
            Indicates whether the term is a real numeral.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsAlgebraicNumber">
            <summary>
            Indicates whether the term is an algebraic number
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBool">
            <summary>
            Indicates whether the term has Boolean sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsTrue">
            <summary>
            Indicates whether the term is the constant true.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsFalse">
            <summary>
            Indicates whether the term is the constant false.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsEq">
            <summary>
            Indicates whether the term is an equality predicate.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsDistinct">
            <summary>
            Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsITE">
            <summary>
            Indicates whether the term is a ternary if-then-else term
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsAnd">
            <summary>
            Indicates whether the term is an n-ary conjunction
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsOr">
            <summary>
            Indicates whether the term is an n-ary disjunction
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsIff">
            <summary>
            Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsXor">
            <summary>
            Indicates whether the term is an exclusive or
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsNot">
            <summary>
            Indicates whether the term is a negation
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsImplies">
            <summary>
            Indicates whether the term is an implication
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsInt">
            <summary>
            Indicates whether the term is of integer sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsReal">
            <summary>
            Indicates whether the term is of sort real.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsArithmeticNumeral">
            <summary>
            Indicates whether the term is an arithmetic numeral.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsLE">
            <summary>
            Indicates whether the term is a less-than-or-equal
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsGE">
            <summary>
            Indicates whether the term is a greater-than-or-equal
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsLT">
            <summary>
            Indicates whether the term is a less-than
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsGT">
            <summary>
            Indicates whether the term is a greater-than
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsAdd">
            <summary>
            Indicates whether the term is addition (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsSub">
            <summary>
            Indicates whether the term is subtraction (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsUMinus">
            <summary>
            Indicates whether the term is a unary minus
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsMul">
            <summary>
            Indicates whether the term is multiplication (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsDiv">
            <summary>
            Indicates whether the term is division (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsIDiv">
            <summary>
            Indicates whether the term is integer division (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRemainder">
            <summary>
            Indicates whether the term is remainder (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsModulus">
            <summary>
            Indicates whether the term is modulus (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsIntToReal">
            <summary>
            Indicates whether the term is a coercion of integer to real (unary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRealToInt">
            <summary>
            Indicates whether the term is a coercion of real to integer (unary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRealIsInt">
            <summary>
            Indicates whether the term is a check that tests whether a real is integral (unary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsArray">
            <summary>
            Indicates whether the term is of an array sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsStore">
            <summary>
            Indicates whether the term is an array store. 
            </summary>
            <remarks>It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). 
            Array store takes at least 3 arguments. </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsSelect">
            <summary>
            Indicates whether the term is an array select.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsConstantArray">
            <summary>
            Indicates whether the term is a constant array.
            </summary>
            <remarks>For example, select(const(v),i) = v holds for every v and i. The function is unary.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsDefaultArray">
            <summary>
            Indicates whether the term is a default array.
            </summary>
            <remarks>For example default(const(v)) = v. The function is unary.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsArrayMap">
            <summary>
            Indicates whether the term is an array map.
            </summary>
            <remarks>It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsAsArray">
            <summary>
            Indicates whether the term is an as-array term.
            </summary>
            <remarks>An as-array term is n array value that behaves as the function graph of the 
            function passed as parameter.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsSetUnion">
            <summary>
            Indicates whether the term is set union
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsSetIntersect">
            <summary>
            Indicates whether the term is set intersection
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsSetDifference">
            <summary>
            Indicates whether the term is set difference
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsSetComplement">
            <summary>
            Indicates whether the term is set complement
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsSetSubset">
            <summary>
            Indicates whether the term is set subset
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBV">
            <summary>
             Indicates whether the terms is of bit-vector sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVNumeral">
            <summary>
            Indicates whether the term is a bit-vector numeral
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVBitOne">
            <summary>
            Indicates whether the term is a one-bit bit-vector with value one
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVBitZero">
            <summary>
            Indicates whether the term is a one-bit bit-vector with value zero
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVUMinus">
            <summary>
            Indicates whether the term is a bit-vector unary minus
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVAdd">
            <summary>
            Indicates whether the term is a bit-vector addition (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSub">
            <summary>
            Indicates whether the term is a bit-vector subtraction (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVMul">
            <summary>
            Indicates whether the term is a bit-vector multiplication (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSDiv">
            <summary>
            Indicates whether the term is a bit-vector signed division (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVUDiv">
            <summary>
            Indicates whether the term is a bit-vector unsigned division (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSRem">
            <summary>
            Indicates whether the term is a bit-vector signed remainder (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVURem">
            <summary>
            Indicates whether the term is a bit-vector unsigned remainder (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSMod">
            <summary>
            Indicates whether the term is a bit-vector signed modulus
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSDiv0">
            <summary>
            Indicates whether the term is a bit-vector signed division by zero
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVUDiv0">
            <summary>
            Indicates whether the term is a bit-vector unsigned division by zero
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSRem0">
            <summary>
            Indicates whether the term is a bit-vector signed remainder by zero
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVURem0">
            <summary>
            Indicates whether the term is a bit-vector unsigned remainder by zero
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSMod0">
            <summary>
            Indicates whether the term is a bit-vector signed modulus by zero
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVULE">
            <summary>
            Indicates whether the term is an unsigned bit-vector less-than-or-equal
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSLE">
            <summary>
            Indicates whether the term is a signed bit-vector less-than-or-equal
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVUGE">
            <summary>
            Indicates whether the term is an unsigned bit-vector greater-than-or-equal
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSGE">
            <summary>
            Indicates whether the term is a signed bit-vector greater-than-or-equal
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVULT">
            <summary>
            Indicates whether the term is an unsigned bit-vector less-than
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSLT">
            <summary>
            Indicates whether the term is a signed bit-vector less-than
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVUGT">
            <summary>
            Indicates whether the term is an unsigned bit-vector greater-than
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSGT">
            <summary>
            Indicates whether the term is a signed bit-vector greater-than
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVAND">
            <summary>
            Indicates whether the term is a bit-wise AND
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVOR">
            <summary>
            Indicates whether the term is a bit-wise OR
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVNOT">
            <summary>
            Indicates whether the term is a bit-wise NOT
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVXOR">
            <summary>
            Indicates whether the term is a bit-wise XOR
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVNAND">
            <summary>
            Indicates whether the term is a bit-wise NAND
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVNOR">
            <summary>
            Indicates whether the term is a bit-wise NOR
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVXNOR">
            <summary>
            Indicates whether the term is a bit-wise XNOR
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVConcat">
            <summary>
            Indicates whether the term is a bit-vector concatenation (binary)
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVSignExtension">
            <summary>
            Indicates whether the term is a bit-vector sign extension
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVZeroExtension">
            <summary>
            Indicates whether the term is a bit-vector zero extension
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVExtract">
            <summary>
            Indicates whether the term is a bit-vector extraction
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVRepeat">
            <summary>
            Indicates whether the term is a bit-vector repetition
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVReduceOR">
            <summary>
            Indicates whether the term is a bit-vector reduce OR
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVReduceAND">
            <summary>
            Indicates whether the term is a bit-vector reduce AND
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVComp">
            <summary>
            Indicates whether the term is a bit-vector comparison
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVShiftLeft">
            <summary>
            Indicates whether the term is a bit-vector shift left
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVShiftRightLogical">
            <summary>
            Indicates whether the term is a bit-vector logical shift right
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVShiftRightArithmetic">
            <summary>
            Indicates whether the term is a bit-vector arithmetic shift left
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVRotateLeft">
            <summary>
            Indicates whether the term is a bit-vector rotate left
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVRotateRight">
            <summary>
            Indicates whether the term is a bit-vector rotate right
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVRotateLeftExtended">
            <summary>
            Indicates whether the term is a bit-vector rotate left (extended)
            </summary>
            <remarks>Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVRotateRightExtended">
            <summary>
            Indicates whether the term is a bit-vector rotate right (extended)
            </summary>
            <remarks>Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsIntToBV">
            <summary>
            Indicates whether the term is a coercion from integer to bit-vector
            </summary>
            <remarks>This function is not supported by the decision procedures. Only the most 
            rudimentary simplification rules are applied to this function.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVToInt">
            <summary>
            Indicates whether the term is a coercion from bit-vector to integer
            </summary>
            <remarks>This function is not supported by the decision procedures. Only the most 
            rudimentary simplification rules are applied to this function.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVCarry">
            <summary>
            Indicates whether the term is a bit-vector carry
            </summary>
            <remarks>Compute the carry bit in a full-adder.  The meaning is given by the 
            equivalence (carry l1 l2 l3) &lt;=&gt; (or (and l1 l2) (and l1 l3) (and l2 l3)))</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsBVXOR3">
            <summary>
            Indicates whether the term is a bit-vector ternary XOR
            </summary>
            <remarks>The meaning is given by the equivalence (xor3 l1 l2 l3) &lt;=&gt; (xor (xor l1 l2) l3)</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsLabel">
            <summary>
            Indicates whether the term is a label (used by the Boogie Verification condition generator).
            </summary>
            <remarks>The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsLabelLit">
            <summary>
            Indicates whether the term is a label literal (used by the Boogie Verification condition generator).                     
            </summary>
            <remarks>A label literal has a set of string parameters. It takes no arguments.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsOEQ">
            <summary>
            Indicates whether the term is a binary equivalence modulo namings. 
            </summary>
            <remarks>This binary predicate is used in proof terms.
            It captures equisatisfiability and equivalence modulo renamings.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofTrue">
            <summary>
            Indicates whether the term is a Proof for the expression 'true'.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofAsserted">
            <summary>
            Indicates whether the term is a proof for a fact asserted by the user.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofGoal">
            <summary>
            Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofModusPonens">
            <summary>
            Indicates whether the term is proof via modus ponens
            </summary>
            <remarks>
            Given a proof for p and a proof for (implies p q), produces a proof for q.
            T1: p
            T2: (implies p q)
            [mp T1 T2]: q
            The second antecedents may also be a proof for (iff p q).</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofReflexivity">
            <summary>
            Indicates whether the term is a proof for (R t t), where R is a reflexive relation.
            </summary>
            <remarks>This proof object has no antecedents. 
            The only reflexive relations that are used are 
            equivalence modulo namings, equality and equivalence.
            That is, R is either '~', '=' or 'iff'.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofSymmetry">
            <summary>
            Indicates whether the term is proof by symmetricity of a relation
            </summary>
            <remarks>
            Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t).
            T1: (R t s)
            [symmetry T1]: (R s t)
            T1 is the antecedent of this proof object.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofTransitivity">
            <summary>
            Indicates whether the term is a proof by transitivity of a relation
            </summary>
            <remarks>
            Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof 
            for (R t u). 
            T1: (R t s)
            T2: (R s u)
            [trans T1 T2]: (R t u)
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofTransitivityStar">
            <summary>
            Indicates whether the term is a proof by condensed transitivity of a relation
            </summary>
            <remarks>
            Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
            It combines several symmetry and transitivity proofs. 
            Example:
            T1: (R a b)
            T2: (R c b)
            T3: (R c d)
            [trans* T1 T2 T3]: (R a d)          
            R must be a symmetric and transitive relation.
            
            Assuming that this proof object is a proof for (R s t), then
            a proof checker must check if it is possible to prove (R s t)
            using the antecedents, symmetry and transitivity.  That is, 
            if there is a path from s to t, if we view every
            antecedent (R a b) as an edge between a and b.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofMonotonicity">
            <summary>
            Indicates whether the term is a monotonicity proof object.
            </summary>
            <remarks>
            T1: (R t_1 s_1)
            ...
            Tn: (R t_n s_n)
            [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))          
            Remark: if t_i == s_i, then the antecedent Ti is suppressed.
            That is, reflexivity proofs are supressed to save space.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofQuantIntro">
            <summary>
            Indicates whether the term is a quant-intro proof 
            </summary>
            <remarks>
            Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
            T1: (~ p q)
            [quant-intro T1]: (~ (forall (x) p) (forall (x) q))
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofDistributivity">
            <summary>
            Indicates whether the term is a distributivity proof object.  
            </summary>
            <remarks>
            Given that f (= or) distributes over g (= and), produces a proof for
            (= (f a (g c d))
            (g (f a c) (f a d)))
            If f and g are associative, this proof also justifies the following equality:
            (= (f (g a b) (g c d))
            (g (f a c) (f a d) (f b c) (f b d)))
            where each f and g can have arbitrary number of arguments.
            
            This proof object has no antecedents.
            Remark. This rule is used by the CNF conversion pass and 
            instantiated by f = or, and g = and.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofAndElimination">
            <summary>
            Indicates whether the term is a proof by elimination of AND
            </summary>
            <remarks>
            Given a proof for (and l_1 ... l_n), produces a proof for l_i
            T1: (and l_1 ... l_n)
            [and-elim T1]: l_i
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofOrElimination">
            <summary>
            Indicates whether the term is a proof by eliminiation of not-or
            </summary>
            <remarks>
            Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
            T1: (not (or l_1 ... l_n))
            [not-or-elim T1]: (not l_i)       
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofRewrite">
            <summary>
            Indicates whether the term is a proof by rewriting
            </summary>
            <remarks>
            A proof for a local rewriting step (= t s).
            The head function symbol of t is interpreted.
            
            This proof object has no antecedents.
            The conclusion of a rewrite rule is either an equality (= t s), 
            an equivalence (iff t s), or equi-satisfiability (~ t s).
            Remark: if f is bool, then = is iff.
            
            Examples:
            (= (+ x 0) x)
            (= (+ x 1 2) (+ 3 x))
            (iff (or x false) x)          
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofRewriteStar">
            <summary>
            Indicates whether the term is a proof by rewriting
            </summary>
            <remarks>
            A proof for rewriting an expression t into an expression s.
            This proof object is used if the parameter PROOF_MODE is 1.
            This proof object can have n antecedents.
            The antecedents are proofs for equalities used as substitution rules.
            The object is also used in a few cases if the parameter PROOF_MODE is 2.
            The cases are:
            - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
            - When converting bit-vectors to Booleans (BIT2BOOL=true)
            - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofPullQuant">
            <summary>
            Indicates whether the term is a proof for pulling quantifiers out.
            </summary>
            <remarks>
            A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofPullQuantStar">
            <summary>
            Indicates whether the term is a proof for pulling quantifiers out.
            </summary>
            <remarks>
            A proof for (iff P Q) where Q is in prenex normal form. 
            This proof object is only used if the parameter PROOF_MODE is 1.       
            This proof object has no antecedents
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofPushQuant">
            <summary>
            Indicates whether the term is a proof for pushing quantifiers in.
            </summary>
            <remarks>
            A proof for:
            (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m]))
                    (and (forall (x_1 ... x_m) p_1[x_1 ... x_m])
                     ... 
                 (forall (x_1 ... x_m) p_n[x_1 ... x_m])))               
             This proof object has no antecedents
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofElimUnusedVars">
            <summary>
            Indicates whether the term is a proof for elimination of unused variables.
            </summary>
            <remarks>
            A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n])
                             (forall (x_1 ... x_n) p[x_1 ... x_n])) 
                             
            It is used to justify the elimination of unused variables.
            This proof object has no antecedents.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofDER">
            <summary>
            Indicates whether the term is a proof for destructive equality resolution
            </summary>
            <remarks>
            A proof for destructive equality resolution:
            (iff (forall (x) (or (not (= x t)) P[x])) P[t])
            if x does not occur in t.
            
            This proof object has no antecedents.
            
            Several variables can be eliminated simultaneously.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofQuantInst">
            <summary>
            Indicates whether the term is a proof for quantifier instantiation
            </summary>
            <remarks>
            A proof of (or (not (forall (x) (P x))) (P a))
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofHypothesis">
            <summary>
            Indicates whether the term is a hypthesis marker.
            </summary>
            <remarks>Mark a hypothesis in a natural deduction style proof.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofLemma">
            <summary>
            Indicates whether the term is a proof by lemma
            </summary>
            <remarks>
            T1: false
            [lemma T1]: (or (not l_1) ... (not l_n))
            
            This proof object has one antecedent: a hypothetical proof for false.
            It converts the proof in a proof for (or (not l_1) ... (not l_n)),
            when T1 contains the hypotheses: l_1, ..., l_n.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofUnitResolution">
            <summary>
            Indicates whether the term is a proof by unit resolution
            </summary>
            <remarks>
            T1:      (or l_1 ... l_n l_1' ... l_m')
            T2:      (not l_1)
            ...
            T(n+1):  (not l_n)
            [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofIFFTrue">
            <summary>
            Indicates whether the term is a proof by iff-true
            </summary>
            <remarks>
            T1: p
            [iff-true T1]: (iff p true)
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofIFFFalse">
            <summary>
            Indicates whether the term is a proof by iff-false
            </summary>
            <remarks>
            T1: (not p)
            [iff-false T1]: (iff p false)
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofCommutativity">
            <summary>
            Indicates whether the term is a proof by commutativity
            </summary>
            <remarks>
            [comm]: (= (f a b) (f b a))
            
            f is a commutative operator.
            
            This proof object has no antecedents.
            Remark: if f is bool, then = is iff.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofDefAxiom">
            <summary>
            Indicates whether the term is a proof for Tseitin-like axioms
            </summary>
            <remarks>
            Proof object used to justify Tseitin's like axioms:
            
            (or (not (and p q)) p)
            (or (not (and p q)) q)
            (or (not (and p q r)) p)
            (or (not (and p q r)) q)
            (or (not (and p q r)) r)
            ...
            (or (and p q) (not p) (not q))
            (or (not (or p q)) p q)
            (or (or p q) (not p))
            (or (or p q) (not q))
            (or (not (iff p q)) (not p) q)
            (or (not (iff p q)) p (not q))
            (or (iff p q) (not p) (not q))
            (or (iff p q) p q)
            (or (not (ite a b c)) (not a) b)
            (or (not (ite a b c)) a c)
            (or (ite a b c) (not a) (not b))
            (or (ite a b c) a (not c))
            (or (not (not a)) (not a))
            (or (not a) a)
            
            This proof object has no antecedents.
            Note: all axioms are propositional tautologies.
            Note also that 'and' and 'or' can take multiple arguments.
            You can recover the propositional tautologies by
            unfolding the Boolean connectives in the axioms a small
            bounded number of steps (=3).
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofDefIntro">
            <summary>
            Indicates whether the term is a proof for introduction of a name
            </summary>
            <remarks>
            Introduces a name for a formula/term.
            Suppose e is an expression with free variables x, and def-intro
            introduces the name n(x). The possible cases are:
            
            When e is of Boolean type:
            [def-intro]: (and (or n (not e)) (or (not n) e))
            
            or:
            [def-intro]: (or (not n) e)
            when e only occurs positively.
            
            When e is of the form (ite cond th el):
            [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))
            
            Otherwise:
            [def-intro]: (= n e)       
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofApplyDef">
            <summary>
            Indicates whether the term is a proof for application of a definition
            </summary>
            <remarks>
             [apply-def T1]: F ~ n
             F is 'equivalent' to n, given that T1 is a proof that
             n is a name for F.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofIFFOEQ">
            <summary>
            Indicates whether the term is a proof iff-oeq
            </summary>
            <remarks>
            T1: (iff p q)
            [iff~ T1]: (~ p q)
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofNNFPos">
             <summary>
             Indicates whether the term is a proof for a positive NNF step
             </summary>
             <remarks>
             Proof for a (positive) NNF step. Example:
             
             T1: (not s_1) ~ r_1
             T2: (not s_2) ~ r_2
             T3: s_1 ~ r_1'
             T4: s_2 ~ r_2'
             [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2)
                                       (and (or r_1 r_2') (or r_1' r_2)))
            
             The negation normal form steps NNF_POS and NNF_NEG are used in the following cases:
             (a) When creating the NNF of a positive force quantifier.
             The quantifier is retained (unless the bound variables are eliminated).
             Example
                T1: q ~ q_new 
                [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))
             
             (b) When recursively creating NNF over Boolean formulas, where the top-level
             connective is changed during NNF conversion. The relevant Boolean connectives
             for NNF_POS are 'implies', 'iff', 'xor', 'ite'.
             NNF_NEG furthermore handles the case where negation is pushed
             over Boolean connectives 'and' and 'or'.
             </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofNNFNeg">
            <summary>
            Indicates whether the term is a proof for a negative NNF step
            </summary>
            <remarks>
            Proof for a (negative) NNF step. Examples:
            
              T1: (not s_1) ~ r_1
              ...
              Tn: (not s_n) ~ r_n
              [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n)
            and
              T1: (not s_1) ~ r_1
              ...
              Tn: (not s_n) ~ r_n
              [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n)
            and
              T1: (not s_1) ~ r_1
              T2: (not s_2) ~ r_2
              T3: s_1 ~ r_1'
              T4: s_2 ~ r_2'
              [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
                                        (and (or r_1 r_2) (or r_1' r_2')))
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofNNFStar">
            <summary>
            Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
            </summary>
            <remarks>
            A proof for (~ P Q) where Q is in negation normal form.
            
            This proof object is only used if the parameter PROOF_MODE is 1.       
            
            This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofCNFStar">
            <summary>
            Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
            </summary>
            <remarks>
            A proof for (~ P Q) where Q is in conjunctive normal form.
            This proof object is only used if the parameter PROOF_MODE is 1.       
            This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.          
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofSkolemize">
            <summary>
            Indicates whether the term is a proof for a Skolemization step
            </summary>
            <remarks>
            Proof for: 
            
              [sk]: (~ (not (forall x (p x y))) (not (p (sk y) y)))
              [sk]: (~ (exists x (p x y)) (p (sk y) y))
              
            This proof object has no antecedents.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofModusPonensOEQ">
            <summary>
            Indicates whether the term is a proof by modus ponens for equi-satisfiability.
            </summary>
            <remarks>
            Modus ponens style rule for equi-satisfiability.
            T1: p
            T2: (~ p q)
            [mp~ T1 T2]: q  
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsProofTheoryLemma">
            <summary>
            Indicates whether the term is a proof for theory lemma
            </summary>
            <remarks>
            Generic proof for theory lemmas.
            
            The theory lemma function comes with one or more parameters.
            The first parameter indicates the name of the theory.
            For the theory of arithmetic, additional parameters provide hints for
            checking the theory lemma. 
            The hints for arithmetic are:
            - farkas - followed by rational coefficients. Multiply the coefficients to the
              inequalities in the lemma, add the (negated) inequalities and obtain a contradiction.
            - triangle-eq - Indicates a lemma related to the equivalence:        
              (iff (= t1 t2) (and (&lt;= t1 t2) (&lt;= t2 t1)))
            - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelation">
            <summary>
            Indicates whether the term is of an array sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelationStore">
            <summary>
            Indicates whether the term is an relation store
            </summary>
            <remarks>
            Insert a record into a relation.
            The function takes <c>n+1</c> arguments, where the first argument is the relation and the remaining <c>n</c> elements 
            correspond to the <c>n</c> columns of the relation.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsEmptyRelation">
            <summary>
            Indicates whether the term is an empty relation
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsIsEmptyRelation">
            <summary>
            Indicates whether the term is a test for the emptiness of a relation
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelationalJoin">
            <summary>
            Indicates whether the term is a relational join
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelationUnion">
            <summary>
            Indicates whether the term is the union or convex hull of two relations. 
            </summary>
            <remarks>The function takes two arguments.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelationWiden">
            <summary>
            Indicates whether the term is the widening of two relations
            </summary>
            <remarks>The function takes two arguments.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelationProject">
            <summary>
            Indicates whether the term is a projection of columns (provided as numbers in the parameters).
            </summary>
            <remarks>The function takes one argument.</remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelationFilter">
            <summary>
            Indicates whether the term is a relation filter
            </summary>
            <remarks>
            Filter (restrict) a relation with respect to a predicate.
            The first argument is a relation. 
            The second argument is a predicate with free de-Brujin indices
            corresponding to the columns of the relation.
            So the first column in the relation has index 0.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelationNegationFilter">
            <summary>
            Indicates whether the term is an intersection of a relation with the negation of another.
            </summary>
            <remarks>
            Intersect the first relation with respect to negation
            of the second relation (the function takes two arguments).
            Logically, the specification can be described by a function
            
              target = filter_by_negation(pos, neg, columns)
              
            where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that
            target are elements in x in pos, such that there is no y in neg that agrees with
            x on the columns c1, d1, .., cN, dN.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelationRename">
            <summary>
            Indicates whether the term is the renaming of a column in a relation
            </summary>
            <remarks>    
            The function takes one argument.
            The parameters contain the renaming as a cycle.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelationComplement">
            <summary>
            Indicates whether the term is the complement of a relation
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelationSelect">
            <summary>
            Indicates whether the term is a relational select
            </summary>
            <remarks>
            Check if a record is an element of the relation.
            The function takes <c>n+1</c> arguments, where the first argument is a relation,
            and the remaining <c>n</c> arguments correspond to a record.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsRelationClone">
            <summary>
            Indicates whether the term is a relational clone (copy)
            </summary>
            <remarks>
            Create a fresh copy (clone) of a relation. 
            The function is logically the identity, but
            in the context of a register machine allows 
            for terms of kind <seealso cref="P:Microsoft.Z3.Expr.IsRelationUnion"/> 
            to perform destructive updates to the first argument.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsFiniteDomain">
            <summary>
            Indicates whether the term is of an array sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.IsFiniteDomainLT">
            <summary>
            Indicates whether the term is a less than predicate over a finite domain.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Expr.Index">
            <summary>
            The de-Burijn index of a bound variable.
            </summary>
            <remarks>
            Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain
            the meaning of de-Bruijn indices by indicating the compilation process from
            non-de-Bruijn formulas to de-Bruijn format.
            <code>
            abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
            abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
            abs1(x, x, n) = b_n
            abs1(y, x, n) = y
            abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
            abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
            </code>
            The last line is significant: the index of a bound variable is different depending
            on the scope in which it appears. The deeper x appears, the higher is its
            index.
            </remarks>
        </member>
        <member name="T:Microsoft.Z3.BoolExpr">
            <summary>
            Boolean expressions
            </summary>
        </member>
        <member name="M:Microsoft.Z3.BoolExpr.#ctor(Microsoft.Z3.Context)">
            <summary> Constructor for BoolExpr </summary>
        </member>
        <member name="M:Microsoft.Z3.BoolExpr.#ctor(Microsoft.Z3.Context,System.IntPtr)">
            <summary> Constructor for BoolExpr </summary>
        </member>
        <member name="T:Microsoft.Z3.ArithExpr">
            <summary>
            Arithmetic expressions (int/real)
            </summary>
        </member>
        <member name="M:Microsoft.Z3.ArithExpr.#ctor(Microsoft.Z3.Context)">
            <summary> Constructor for ArithExpr </summary>
        </member>
        <member name="T:Microsoft.Z3.IntExpr">
            <summary>
            Int expressions
            </summary>
        </member>
        <member name="M:Microsoft.Z3.IntExpr.#ctor(Microsoft.Z3.Context)">
            <summary> Constructor for IntExpr </summary>
        </member>
        <member name="T:Microsoft.Z3.RealExpr">
            <summary>
            Real expressions
            </summary>
        </member>
        <member name="M:Microsoft.Z3.RealExpr.#ctor(Microsoft.Z3.Context)">
            <summary> Constructor for RealExpr </summary>
        </member>
        <member name="T:Microsoft.Z3.BitVecExpr">
            <summary>
            Bit-vector expressions
            </summary>
        </member>
        <member name="M:Microsoft.Z3.BitVecExpr.#ctor(Microsoft.Z3.Context)">
            <summary> Constructor for BitVecExpr </summary>
        </member>
        <member name="P:Microsoft.Z3.BitVecExpr.SortSize">
            <summary>
            The size of the sort of a bit-vector term.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.ArrayExpr">
            <summary>
            Array expressions
            </summary>
        </member>
        <member name="M:Microsoft.Z3.ArrayExpr.#ctor(Microsoft.Z3.Context)">
            <summary> Constructor for ArrayExpr </summary>
        </member>
        <member name="T:Microsoft.Z3.DatatypeExpr">
            <summary>
            Datatype expressions
            </summary>
        </member>
        <member name="M:Microsoft.Z3.DatatypeExpr.#ctor(Microsoft.Z3.Context)">
            <summary> Constructor for DatatypeExpr </summary>
        </member>
        <member name="T:Microsoft.Z3.Version">
            <summary>
            Version information.
            </summary>
            <remarks>Note that this class is static.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Version.ToString">
            <summary>
            A string representation of the version information.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Version.Major">
            <summary>
            The major version
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Version.Minor">
            <summary>
            The minor version
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Version.Build">
            <summary>
            The build version
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Version.Revision">
            <summary>
            The revision
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Model">
            <summary>
            A Model contains interpretations (assignments) of constants and functions. 
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Model.ConstInterp(Microsoft.Z3.Expr)">
            <summary>
            Retrieves the interpretation (the assignment) of <paramref name="a"/> in the model. 
            </summary>
            <param name="a">A Constant</param>
            <returns>An expression if the constant has an interpretation in the model, null otherwise.</returns>
        </member>
        <member name="M:Microsoft.Z3.Model.ConstInterp(Microsoft.Z3.FuncDecl)">
            <summary>
            Retrieves the interpretation (the assignment) of <paramref name="f"/> in the model. 
            </summary>
            <param name="f">A function declaration of zero arity</param>
            <returns>An expression if the function has an interpretation in the model, null otherwise.</returns>    
        </member>
        <member name="M:Microsoft.Z3.Model.FuncInterp(Microsoft.Z3.FuncDecl)">
            <summary>
            Retrieves the interpretation (the assignment) of a non-constant <paramref name="f"/> in the model. 
            </summary>
            <param name="f">A function declaration of non-zero arity</param>
            <returns>A FunctionInterpretation if the function has an interpretation in the model, null otherwise.</returns> 
        </member>
        <member name="M:Microsoft.Z3.Model.Eval(Microsoft.Z3.Expr,System.Boolean)">
            <summary>
            Evaluates the expression <paramref name="t"/> in the current model.
            </summary>
            <remarks>
            This function may fail if <paramref name="t"/> contains quantifiers, 
            is partial (MODEL_PARTIAL enabled), or if <paramref name="t"/> is not well-sorted.
            In this case a <c>ModelEvaluationFailedException</c> is thrown.
            </remarks>
            <param name="t">An expression</param>
            <param name="completion">
            When this flag is enabled, a model value will be assigned to any constant 
            or function that does not have an interpretation in the model.
            </param>
            <returns>The evaluation of <paramref name="t"/> in the model.</returns>        
        </member>
        <member name="M:Microsoft.Z3.Model.Evaluate(Microsoft.Z3.Expr,System.Boolean)">
            <summary>
            Alias for <c>Eval</c>.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Model.SortUniverse(Microsoft.Z3.Sort)">
            <summary>
            The finite set of distinct values that represent the interpretation for sort <paramref name="s"/>.
            </summary>
            <seealso cref="P:Microsoft.Z3.Model.Sorts"/>
            <param name="s">An uninterpreted sort</param>
            <returns>An array of expressions, where each is an element of the universe of <paramref name="s"/></returns>
        </member>
        <member name="M:Microsoft.Z3.Model.ToString">
            <summary>
            Conversion of models to strings. 
            </summary>
            <returns>A string representation of the model.</returns>
        </member>
        <member name="P:Microsoft.Z3.Model.NumConsts">
            <summary>
            The number of constants that have an interpretation in the model.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Model.ConstDecls">
            <summary>
            The function declarations of the constants in the model.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Model.NumFuncs">
            <summary>
            The number of function interpretations in the model.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Model.FuncDecls">
            <summary>
            The function declarations of the function interpretations in the model.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Model.Decls">
            <summary>
            All symbols that have an interpretation in the model.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Model.NumSorts">
            <summary>
            The number of uninterpreted sorts that the model has an interpretation for.
            </summary>    
        </member>
        <member name="P:Microsoft.Z3.Model.Sorts">
            <summary>
            The uninterpreted sorts that the model has an interpretation for. 
            </summary>
            <remarks>
            Z3 also provides an intepretation for uninterpreted sorts used in a formula.
            The interpretation for a sort is a finite set of distinct values. We say this finite set is
            the "universe" of the sort.
            </remarks>
            <seealso cref="P:Microsoft.Z3.Model.NumSorts"/>
            <seealso cref="M:Microsoft.Z3.Model.SortUniverse(Microsoft.Z3.Sort)"/>
        </member>
        <member name="T:Microsoft.Z3.Model.ModelEvaluationFailedException">
            <summary>
            A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Z3Exception">
            <summary>
            The exception base class for error reporting from Z3
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Z3Exception.#ctor">
            <summary>
            Constructor.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Z3Exception.#ctor(System.String)">
            <summary>
            Constructor.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Z3Exception.#ctor(System.String,System.Exception)">
            <summary>
            Constructor.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Model.ModelEvaluationFailedException.#ctor">
            <summary>
            An exception that is thrown when model evaluation fails.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Goal">
            <summary>
            A goal (aka problem). A goal is essentially a set
            of formulas, that can be solved and/or transformed using
            tactics and solvers.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Goal.Assert(Microsoft.Z3.BoolExpr[])">
            <summary>
            Adds the <paramref name="constraints"/> to the given goal. 
            </summary>   
        </member>
        <member name="M:Microsoft.Z3.Goal.Reset">
            <summary>
            Erases all formulas from the given goal.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Goal.Translate(Microsoft.Z3.Context)">
            <summary>
            Translates (copies) the Goal to the target Context <paramref name="ctx"/>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Goal.Simplify(Microsoft.Z3.Params)">
            <summary>
            Simplifies the goal.
            </summary>
            <remarks>Essentially invokes the `simplify' tactic on the goal.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Goal.ToString">
            <summary>
            Goal to string conversion.
            </summary>
            <returns>A string representation of the Goal.</returns>
        </member>
        <member name="P:Microsoft.Z3.Goal.Precision">
            <summary>
            The precision of the goal. 
            </summary>
            <remarks>
            Goals can be transformed using over and under approximations.
            An under approximation is applied when the objective is to find a model for a given goal.
            An over approximation is applied when the objective is to find a proof for a given goal.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Goal.IsPrecise">
            <summary>
            Indicates whether the goal is precise.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Goal.IsUnderApproximation">
            <summary>
            Indicates whether the goal is an under-approximation.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Goal.IsOverApproximation">
            <summary>
            Indicates whether the goal is an over-approximation.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Goal.IsGarbage">
            <summary>
            Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Goal.Inconsistent">
            <summary>
            Indicates whether the goal contains `false'.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Goal.Depth">
            <summary>
            The depth of the goal.
            </summary>
            <remarks>
            This tracks how many transformations were applied to it.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Goal.Size">
            <summary>
            The number of formulas in the goal.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Goal.Formulas">
            <summary>
            The formulas in the goal.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Goal.NumExprs">
            <summary>
            The number of formulas, subformulas and terms in the goal.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Goal.IsDecidedSat">
            <summary>
            Indicates whether the goal is empty, and it is precise or the product of an under approximation.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Goal.IsDecidedUnsat">
            <summary>
            Indicates whether the goal contains `false', and it is precise or the product of an over approximation.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.FuncInterp">
            <summary>
             A function interpretation is represented as a finite map and an 'else' value.
             Each entry in the finite map represents the value of a function given a set of arguments.  
            </summary>
        </member>
        <member name="M:Microsoft.Z3.FuncInterp.ToString">
            <summary>
            A string representation of the function interpretation.
            </summary>    
        </member>
        <member name="P:Microsoft.Z3.FuncInterp.NumEntries">
            <summary>
            The number of entries in the function interpretation.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncInterp.Entries">
            <summary>
            The entries in the function interpretation
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncInterp.Else">
            <summary>
            The (symbolic) `else' value of the function interpretation.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncInterp.Arity">
            <summary>
            The arity of the function interpretation
            </summary>
        </member>
        <member name="T:Microsoft.Z3.FuncInterp.Entry">
            <summary>
            An Entry object represents an element in the finite map used to encode
            a function interpretation.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.FuncInterp.Entry.ToString">
            <summary>
            A string representation of the function entry.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncInterp.Entry.Value">
            <summary>
            Return the (symbolic) value of this entry.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncInterp.Entry.NumArgs">
            <summary>
            The number of arguments of the entry.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncInterp.Entry.Args">
            <summary>
            The arguments of the function entry.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.ASTVector">
            <summary>
            Vectors of ASTs.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.ASTVector.Resize(System.UInt32)">
            <summary>
            Resize the vector to <paramref name="newSize"/>.
            </summary>
            <param name="newSize">The new size of the vector.</param>
        </member>
        <member name="M:Microsoft.Z3.ASTVector.Push(Microsoft.Z3.AST)">
            <summary>
            Add the AST <paramref name="a"/> to the back of the vector. The size
            is increased by 1.
            </summary>
            <param name="a">An AST</param>
        </member>
        <member name="M:Microsoft.Z3.ASTVector.Translate(Microsoft.Z3.Context)">
            <summary>
            Translates all ASTs in the vector to <paramref name="ctx"/>.
            </summary>
            <param name="ctx">A context</param>
            <returns>A new ASTVector</returns>
        </member>
        <member name="M:Microsoft.Z3.ASTVector.ToString">
            <summary>
            Retrieves a string representation of the vector. 
            </summary>    
        </member>
        <member name="P:Microsoft.Z3.ASTVector.Size">
            <summary>
            The size of the vector
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ASTVector.Item(System.UInt32)">
            <summary>
            Retrieves the i-th object in the vector.
            </summary>
            <remarks>May throw an IndexOutOfBoundsException when <paramref name="i"/> is out of range.</remarks>
            <param name="i">Index</param>
            <returns>An AST</returns>
        </member>
        <member name="T:Microsoft.Z3.Sort">
            <summary>
            The Sort class implements type information for ASTs.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Sort.op_Equality(Microsoft.Z3.Sort,Microsoft.Z3.Sort)">
            <summary>
            Comparison operator.
            </summary>
            <param name="a">A Sort</param>
            <param name="b">A Sort</param>
            <returns>True if <paramref name="a"/> and <paramref name="b"/> are from the same context 
            and represent the same sort; false otherwise.</returns>
        </member>
        <member name="M:Microsoft.Z3.Sort.op_Inequality(Microsoft.Z3.Sort,Microsoft.Z3.Sort)">
            <summary>
            Comparison operator.
            </summary>
            <param name="a">A Sort</param>
            <param name="b">A Sort</param>
            <returns>True if <paramref name="a"/> and <paramref name="b"/> are not from the same context 
            or represent different sorts; false otherwise.</returns>
        </member>
        <member name="M:Microsoft.Z3.Sort.Equals(System.Object)">
            <summary>
            Equality operator for objects of type Sort.
            </summary>
            <param name="o"></param>
            <returns></returns>
        </member>
        <member name="M:Microsoft.Z3.Sort.GetHashCode">
            <summary>
            Hash code generation for Sorts
            </summary>
            <returns>A hash code</returns>
        </member>
        <member name="M:Microsoft.Z3.Sort.ToString">
            <summary>
            A string representation of the sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Sort.#ctor(Microsoft.Z3.Context)">
            <summary>
            Sort constructor
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Sort.Id">
            <summary>
            Returns a unique identifier for the sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Sort.SortKind">
            <summary>
            The kind of the sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Sort.Name">
            <summary>
            The name of the sort
            </summary>
        </member>
        <member name="T:Microsoft.Z3.BoolSort">
            <summary>
            A Boolean sort.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.ArithSort">
            <summary>
            An arithmetic sort, i.e., Int or Real.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.IntSort">
            <summary>
             An Integer sort
            </summary>
        </member>
        <member name="T:Microsoft.Z3.RealSort">
            <summary>
            A real sort
            </summary>
        </member>
        <member name="T:Microsoft.Z3.BitVecSort">
            <summary>
            Bit-vector sorts.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.BitVecSort.Size">
            <summary>
            The size of the bit-vector sort.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.ArraySort">
            <summary>
            Array sorts.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ArraySort.Domain">
            <summary>
            The domain of the array sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ArraySort.Range">
            <summary>
            The range of the array sort.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.DatatypeSort">
            <summary>
            Datatype sorts.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.DatatypeSort.NumConstructors">
            <summary>
            The number of constructors of the datatype sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.DatatypeSort.Constructors">
            <summary>
            The constructors.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.DatatypeSort.Recognizers">
            <summary>
            The recognizers.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.DatatypeSort.Accessors">
            <summary>
            The constructor accessors.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.UninterpretedSort">
            <summary>
            Uninterpreted Sorts
            </summary>
        </member>
        <member name="T:Microsoft.Z3.TupleSort">
            <summary>
            Tuple sorts.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.TupleSort.MkDecl">
            <summary>
            The constructor function of the tuple.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.TupleSort.NumFields">
            <summary>
            The number of fields in the tuple.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.TupleSort.FieldDecls">
            <summary>
            The field declarations.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.EnumSort">
            <summary>
            Enumeration sorts.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.EnumSort.ConstDecls">
            <summary>
            The function declarations of the constants in the enumeration.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.EnumSort.Consts">
            <summary>
            The constants in the enumeration.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.EnumSort.TesterDecls">
            <summary>
            The test predicates for the constants in the enumeration.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.ListSort">
            <summary>
            List sorts.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ListSort.NilDecl">
            <summary>
            The declaration of the nil function of this list sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ListSort.Nil">
            <summary>
            The empty list.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ListSort.IsNilDecl">
            <summary>
            The declaration of the isNil function of this list sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ListSort.ConsDecl">
            <summary>
            The declaration of the cons function of this list sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ListSort.IsConsDecl">
            <summary>
            The declaration of the isCons function of this list sort.
            </summary>
            
        </member>
        <member name="P:Microsoft.Z3.ListSort.HeadDecl">
            <summary>
            The declaration of the head function of this list sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ListSort.TailDecl">
            <summary>
            The declaration of the tail function of this list sort.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.RelationSort">
            <summary>
            Relation sorts.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.RelationSort.Arity">
            <summary>
            The arity of the relation sort.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.RelationSort.ColumnSorts">
            <summary>
            The sorts of the columns of the relation sort.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.FiniteDomainSort">
            <summary>
            Finite domain sorts.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FiniteDomainSort.Size">
            <summary>
            The size of the finite domain sort.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.SetSort">
            <summary>
            Set sorts.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Tactic">
            <summary>
            Tactics are the basic building block for creating custom solvers for specific problem domains.
            The complete list of tactics may be obtained using <c>Context.NumTactics</c> 
            and <c>Context.TacticNames</c>.
            It may also be obtained using the command <c>(help-tactics)</c> in the SMT 2.0 front-end.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Tactic.Apply(Microsoft.Z3.Goal,Microsoft.Z3.Params)">
            <summary>
            Execute the tactic over the goal. 
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Tactic.Help">
            <summary>
            A string containing a description of parameters accepted by the tactic.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Tactic.Item(Microsoft.Z3.Goal)">
            <summary>
            Apply the tactic to a goal.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Tactic.Solver">
            <summary>
            Creates a solver that is implemented using the given tactic.
            </summary>
            <seealso cref="M:Microsoft.Z3.Context.MkSolver(Microsoft.Z3.Tactic)"/>
        </member>
        <member name="T:Microsoft.Z3.Symbol">
            <summary>
            Symbols are used to name several term and type constructors.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Symbol.IsIntSymbol">
            <summary>
            Indicates whether the symbol is of Int kind
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Symbol.IsStringSymbol">
            <summary>
            Indicates whether the symbol is of string kind.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Symbol.ToString">
            <summary>
            A string representation of the symbol.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Symbol.#ctor(Microsoft.Z3.Context,System.IntPtr)">
            <summary>
            Symbol constructor
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Symbol.Kind">
            <summary>
            The kind of the symbol (int or string)
            </summary>
        </member>
        <member name="T:Microsoft.Z3.IntSymbol">
            <summary>
            Numbered symbols
            </summary>
        </member>
        <member name="P:Microsoft.Z3.IntSymbol.Int">
            <summary>
            The int value of the symbol.
            </summary>
            <remarks>Throws an exception if the symbol is not of int kind. </remarks>
        </member>
        <member name="T:Microsoft.Z3.StringSymbol">
            <summary>
            Named symbols
            </summary>
        </member>
        <member name="P:Microsoft.Z3.StringSymbol.String">
            <summary>
            The string value of the symbol.
            </summary>
            <remarks>Throws an exception if the symbol is not of string kind.</remarks>
        </member>
        <member name="T:Microsoft.Z3.Pattern">
            <summary>
            Patterns comprise a list of terms. The list should be
            non-empty.  If the list comprises of more than one term, it is
            also called a multi-pattern.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Pattern.ToString">
            <summary>
            A string representation of the pattern.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Pattern.NumTerms">
            <summary>
            The number of terms in the pattern.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Pattern.Terms">
            <summary>
            The terms in the pattern.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.ASTMap">
            <summary>
            Map from AST to AST
            </summary>
        </member>
        <member name="M:Microsoft.Z3.ASTMap.Contains(Microsoft.Z3.AST)">
            <summary>
            Checks whether the map contains the key <paramref name="k"/>.
            </summary>
            <param name="k">An AST</param>
            <returns>True if <paramref name="k"/> is a key in the map, false otherwise.</returns>
        </member>
        <member name="M:Microsoft.Z3.ASTMap.Find(Microsoft.Z3.AST)">
            <summary>
            Finds the value associated with the key <paramref name="k"/>.
            </summary>
            <remarks>
            This function signs an error when <paramref name="k"/> is not a key in the map.
            </remarks>
            <param name="k">An AST</param>    
        </member>
        <member name="M:Microsoft.Z3.ASTMap.Insert(Microsoft.Z3.AST,Microsoft.Z3.AST)">
            <summary>
            Stores or replaces a new key/value pair in the map.
            </summary>
            <param name="k">The key AST</param>
            <param name="v">The value AST</param>
        </member>
        <member name="M:Microsoft.Z3.ASTMap.Erase(Microsoft.Z3.AST)">
            <summary>
            Erases the key <paramref name="k"/> from the map.
            </summary>
            <param name="k">An AST</param>
        </member>
        <member name="M:Microsoft.Z3.ASTMap.Reset">
            <summary>
            Removes all keys from the map.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.ASTMap.ToString">
            <summary>
            Retrieves a string representation of the map. 
            </summary>    
        </member>
        <member name="P:Microsoft.Z3.ASTMap.Size">
            <summary>
            The size of the map
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ASTMap.Keys">
            <summary>
            The keys stored in the map.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Quantifier">
            <summary>
            Quantifier expressions.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Quantifier.IsUniversal">
            <summary>
            Indicates whether the quantifier is universal.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Quantifier.IsExistential">
            <summary>
            Indicates whether the quantifier is existential.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Quantifier.Weight">
            <summary>
            The weight of the quantifier.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Quantifier.NumPatterns">
            <summary>
            The number of patterns.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Quantifier.Patterns">
            <summary>
            The patterns.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Quantifier.NumNoPatterns">
            <summary>
            The number of no-patterns.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Quantifier.NoPatterns">
            <summary>
            The no-patterns.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Quantifier.NumBound">
            <summary>
            The number of bound variables.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Quantifier.BoundVariableNames">
            <summary>
            The symbols for the bound variables.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Quantifier.BoundVariableSorts">
            <summary>
            The sorts of the bound variables.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Quantifier.Body">
            <summary>
            The body of the quantifier.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Solver">
            <summary>
            Solvers.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Solver.Push">
            <summary>
            Creates a backtracking point.
            </summary>
            <seealso cref="M:Microsoft.Z3.Solver.Pop(System.UInt32)"/>
        </member>
        <member name="M:Microsoft.Z3.Solver.Pop(System.UInt32)">
            <summary>
            Backtracks <paramref name="n"/> backtracking points.
            </summary>
            <remarks>Note that an exception is thrown if <paramref name="n"/> is not smaller than <c>NumScopes</c></remarks>
            <seealso cref="M:Microsoft.Z3.Solver.Push"/>
        </member>
        <member name="M:Microsoft.Z3.Solver.Reset">
            <summary>
            Resets the Solver.
            </summary>
            <remarks>This removes all assertions from the solver.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Solver.Assert(Microsoft.Z3.BoolExpr[])">
            <summary>
            Assert a constraint (or multiple) into the solver.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Solver.Check(Microsoft.Z3.Expr[])">
            <summary>
            Checks whether the assertions in the solver are consistent or not.
            </summary>
            <remarks>
            <seealso cref="P:Microsoft.Z3.Solver.Model"/>
            <seealso cref="P:Microsoft.Z3.Solver.UnsatCore"/>
            <seealso cref="P:Microsoft.Z3.Solver.Proof"/>    
            </remarks>    
        </member>
        <member name="M:Microsoft.Z3.Solver.ToString">
            <summary>
            A string representation of the solver.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Solver.Help">
            <summary>
            A string that describes all available solver parameters.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Solver.Parameters">
            <summary>
            Sets the solver parameters.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Solver.NumScopes">
            <summary>
            The current number of backtracking points (scopes).
            </summary>
            <seealso cref="M:Microsoft.Z3.Solver.Pop(System.UInt32)"/>
            <seealso cref="M:Microsoft.Z3.Solver.Push"/>
        </member>
        <member name="P:Microsoft.Z3.Solver.NumAssertions">
            <summary>
            The number of assertions in the solver.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Solver.Assertions">
            <summary>
            The set of asserted formulas.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Solver.Model">
            <summary>
            The model of the last <c>Check</c>.
            </summary>
            <remarks>
            The result is <c>null</c> if <c>Check</c> was not invoked before,
            if its results was not <c>SATISFIABLE</c>, or if model production is not enabled.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Solver.Proof">
            <summary>
            The proof of the last <c>Check</c>.
            </summary>
            <remarks>    
            The result is <c>null</c> if <c>Check</c> was not invoked before,
            if its results was not <c>UNSATISFIABLE</c>, or if proof production is disabled.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Solver.UnsatCore">
            <summary>
            The unsat core of the last <c>Check</c>.
            </summary>
            <remarks>
            The unsat core is a subset of <c>Assertions</c>
            The result is empty if <c>Check</c> was not invoked before,
            if its results was not <c>UNSATISFIABLE</c>, or if core production is disabled.
            </remarks>
        </member>
        <member name="P:Microsoft.Z3.Solver.ReasonUnknown">
            <summary>
            A brief justification of why the last call to <c>Check</c> returned <c>UNKNOWN</c>.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Solver.Statistics">
            <summary>
            Solver statistics.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Context">
            <summary>
            The main interaction with Z3 happens via the Context.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.#ctor">
            <summary>
            Constructor.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.#ctor(System.Collections.Generic.Dictionary{System.String,System.String})">
            <summary>
            Constructor.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSymbol(System.Int32)">
            <summary>
            Creates a new symbol using an integer.
            </summary>
            <remarks>
            Not all integers can be passed to this function.
            The legal range of unsigned integers is 0 to 2^30-1.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSymbol(System.String)">
            <summary>
            Create a symbol using a string.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSymbols(System.String[])">
            <summary>
            Create an array of symbols.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBoolSort">
            <summary>
            Create a new Boolean sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkUninterpretedSort(Microsoft.Z3.Symbol)">
            <summary>
            Create a new uninterpreted sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkUninterpretedSort(System.String)">
            <summary>
            Create a new uninterpreted sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkIntSort">
            <summary>
            Create a new integer sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkRealSort">
            <summary>
            Create a real sort.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkBitVecSort(System.UInt32)">
            <summary>
            Create a new bit-vector sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkArraySort(Microsoft.Z3.Sort,Microsoft.Z3.Sort)">
            <summary>
            Create a new array sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkTupleSort(Microsoft.Z3.Symbol,Microsoft.Z3.Symbol[],Microsoft.Z3.Sort[])">
            <summary>
            Create a new tuple sort.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkEnumSort(Microsoft.Z3.Symbol,Microsoft.Z3.Symbol[])">
            <summary>
            Create a new enumeration sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkEnumSort(System.String,System.String[])">
            <summary>
            Create a new enumeration sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkListSort(Microsoft.Z3.Symbol,Microsoft.Z3.Sort)">
            <summary>
            Create a new list sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkListSort(System.String,Microsoft.Z3.Sort)">
            <summary>
            Create a new list sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkFiniteDomainSort(Microsoft.Z3.Symbol,System.UInt64)">
            <summary>
            Create a new finite domain sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkFiniteDomainSort(System.String,System.UInt64)">
            <summary>
            Create a new finite domain sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkConstructor(Microsoft.Z3.Symbol,Microsoft.Z3.Symbol,Microsoft.Z3.Symbol[],Microsoft.Z3.Sort[],System.UInt32[])">
            <summary>
            Create a datatype constructor.
            </summary>
            <param name="name">constructor name</param>
            <param name="recognizer">name of recognizer function.</param>
            <param name="fieldNames">names of the constructor fields.</param>
            <param name="sorts">field sorts, 0 if the field sort refers to a recursive sort.</param>
            <param name="sortRefs">reference to datatype sort that is an argument to the constructor; 
            if the corresponding sort reference is 0, then the value in sort_refs should be an index 
            referring to one of the recursive datatypes that is declared.</param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkConstructor(System.String,System.String,System.String[],Microsoft.Z3.Sort[],System.UInt32[])">
            <summary>
            Create a datatype constructor.
            </summary>
            <param name="name"></param>
            <param name="recognizer"></param>
            <param name="fieldNames"></param>
            <param name="sorts"></param>
            <param name="sortRefs"></param>
            <returns></returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkDatatypeSort(Microsoft.Z3.Symbol,Microsoft.Z3.Constructor[])">
            <summary>
            Create a new datatype sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkDatatypeSort(System.String,Microsoft.Z3.Constructor[])">
            <summary>
            Create a new datatype sort.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkDatatypeSorts(Microsoft.Z3.Symbol[],Microsoft.Z3.Constructor[][])">
            <summary>
            Create mutually recursive datatypes.
            </summary>
            <param name="names">names of datatype sorts</param>
            <param name="c">list of constructors, one list per sort.</param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkDatatypeSorts(System.String[],Microsoft.Z3.Constructor[][])">
            <summary>
             Create mutually recursive data-types.
            </summary>
            <param name="names"></param>
            <param name="c"></param>
            <returns></returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkFuncDecl(Microsoft.Z3.Symbol,Microsoft.Z3.Sort[],Microsoft.Z3.Sort)">
            <summary>
            Creates a new function declaration.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkFuncDecl(Microsoft.Z3.Symbol,Microsoft.Z3.Sort,Microsoft.Z3.Sort)">
            <summary>
            Creates a new function declaration.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkFuncDecl(System.String,Microsoft.Z3.Sort[],Microsoft.Z3.Sort)">
            <summary>
            Creates a new function declaration.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkFuncDecl(System.String,Microsoft.Z3.Sort,Microsoft.Z3.Sort)">
            <summary>
            Creates a new function declaration.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkFreshFuncDecl(System.String,Microsoft.Z3.Sort[],Microsoft.Z3.Sort)">
            <summary>
            Creates a fresh function declaration with a name prefixed with <paramref name="prefix"/>.
            </summary>
            <seealso cref="M:Microsoft.Z3.Context.MkFuncDecl(System.String,Microsoft.Z3.Sort,Microsoft.Z3.Sort)"/>
            <seealso cref="M:Microsoft.Z3.Context.MkFuncDecl(System.String,Microsoft.Z3.Sort[],Microsoft.Z3.Sort)"/>
        </member>
        <member name="M:Microsoft.Z3.Context.MkConstDecl(Microsoft.Z3.Symbol,Microsoft.Z3.Sort)">
            <summary>
            Creates a new constant function declaration.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkConstDecl(System.String,Microsoft.Z3.Sort)">
            <summary>
            Creates a new constant function declaration.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkFreshConstDecl(System.String,Microsoft.Z3.Sort)">
            <summary>
            Creates a fresh constant function declaration with a name prefixed with <paramref name="prefix"/>.
            </summary>
            <seealso cref="M:Microsoft.Z3.Context.MkFuncDecl(System.String,Microsoft.Z3.Sort,Microsoft.Z3.Sort)"/>
            <seealso cref="M:Microsoft.Z3.Context.MkFuncDecl(System.String,Microsoft.Z3.Sort[],Microsoft.Z3.Sort)"/>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBound(System.UInt32,Microsoft.Z3.Sort)">
            <summary>
            Creates a new bound variable.
            </summary>
            <param name="index">The de-Bruijn index of the variable</param>
            <param name="ty">The sort of the variable</param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkPattern(Microsoft.Z3.Expr[])">
            <summary>
            Create a quantifier pattern.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkConst(Microsoft.Z3.Symbol,Microsoft.Z3.Sort)">
            <summary>
            Creates a new Constant of sort <paramref name="range"/> and named <paramref name="name"/>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkConst(System.String,Microsoft.Z3.Sort)">
            <summary>
            Creates a new Constant of sort <paramref name="range"/> and named <paramref name="name"/>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkFreshConst(System.String,Microsoft.Z3.Sort)">
            <summary>
            Creates a fresh Constant of sort <paramref name="range"/> and a 
            name prefixed with <paramref name="prefix"/>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkConst(Microsoft.Z3.FuncDecl)">
            <summary>
            Creates a fresh constant from the FuncDecl <paramref name="f"/>.
            </summary>
            <param name="f">A decl of a 0-arity function</param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBoolConst(Microsoft.Z3.Symbol)">
            <summary>
            Create a Boolean constant.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Context.MkBoolConst(System.String)">
            <summary>
            Create a Boolean constant.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Context.MkIntConst(Microsoft.Z3.Symbol)">
            <summary>
            Creates an integer constant.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Context.MkIntConst(System.String)">
            <summary>
            Creates an integer constant.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkRealConst(Microsoft.Z3.Symbol)">
            <summary>
            Creates a real constant.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkRealConst(System.String)">
            <summary>
            Creates a real constant.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVConst(Microsoft.Z3.Symbol,System.UInt32)">
            <summary>
            Creates a bit-vector constant.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVConst(System.String,System.UInt32)">
            <summary>
            Creates a bit-vector constant.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkApp(Microsoft.Z3.FuncDecl,Microsoft.Z3.Expr[])">
            <summary>
            Create a new function application.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkTrue">
            <summary>
            The true Term.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkFalse">
            <summary>
            The false Term.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkBool(System.Boolean)">
            <summary>
            Creates a Boolean value.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Context.MkEq(Microsoft.Z3.Expr,Microsoft.Z3.Expr)">
            <summary>
            Creates the equality <paramref name="x"/> = <paramref name="y"/>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkDistinct(Microsoft.Z3.Expr[])">
            <summary>
            Creates a <c>distinct</c> term.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkNot(Microsoft.Z3.BoolExpr)">
            <summary>
             Mk an expression representing <c>not(a)</c>.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkITE(Microsoft.Z3.BoolExpr,Microsoft.Z3.Expr,Microsoft.Z3.Expr)">
            <summary>    
             Create an expression representing an if-then-else: <c>ite(t1, t2, t3)</c>.
            </summary>
            <param name="t1">An expression with Boolean sort</param>
            <param name="t2">An expression </param>
            <param name="t3">An expression with the same sort as <paramref name="t2"/></param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkIff(Microsoft.Z3.BoolExpr,Microsoft.Z3.BoolExpr)">
            <summary>
            Create an expression representing <c>t1 iff t2</c>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkImplies(Microsoft.Z3.BoolExpr,Microsoft.Z3.BoolExpr)">
            <summary>
            Create an expression representing <c>t1 -> t2</c>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkXor(Microsoft.Z3.BoolExpr,Microsoft.Z3.BoolExpr)">
            <summary>
            Create an expression representing <c>t1 xor t2</c>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkAnd(Microsoft.Z3.BoolExpr[])">
            <summary>
            Create an expression representing <c>t[0] and t[1] and ...</c>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkOr(Microsoft.Z3.BoolExpr[])">
            <summary>
            Create an expression representing <c>t[0] or t[1] or ...</c>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkAdd(Microsoft.Z3.ArithExpr[])">
            <summary>
            Create an expression representing <c>t[0] + t[1] + ...</c>.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkMul(Microsoft.Z3.ArithExpr[])">
            <summary>
            Create an expression representing <c>t[0] * t[1] * ...</c>.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkSub(Microsoft.Z3.ArithExpr[])">
            <summary>
            Create an expression representing <c>t[0] - t[1] - ...</c>.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkUnaryMinus(Microsoft.Z3.ArithExpr)">
            <summary>
            Create an expression representing <c>-t</c>.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkDiv(Microsoft.Z3.ArithExpr,Microsoft.Z3.ArithExpr)">
            <summary>
            Create an expression representing <c>t1 / t2</c>.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkMod(Microsoft.Z3.IntExpr,Microsoft.Z3.IntExpr)">
            <summary>
            Create an expression representing <c>t1 mod t2</c>.
            </summary>
            <remarks>The arguments must have int type.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkRem(Microsoft.Z3.IntExpr,Microsoft.Z3.IntExpr)">
            <summary>
            Create an expression representing <c>t1 rem t2</c>.
            </summary>
            <remarks>The arguments must have int type.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkPower(Microsoft.Z3.ArithExpr,Microsoft.Z3.ArithExpr)">
            <summary>
            Create an expression representing <c>t1 ^ t2</c>.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkLt(Microsoft.Z3.ArithExpr,Microsoft.Z3.ArithExpr)">
            <summary>
            Create an expression representing <c>t1 &lt; t2</c>
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkLe(Microsoft.Z3.ArithExpr,Microsoft.Z3.ArithExpr)">
            <summary>
            Create an expression representing <c>t1 &lt;= t2</c>
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkGt(Microsoft.Z3.ArithExpr,Microsoft.Z3.ArithExpr)">
            <summary>
            Create an expression representing <c>t1 &gt; t2</c>
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkGe(Microsoft.Z3.ArithExpr,Microsoft.Z3.ArithExpr)">
            <summary>
            Create an expression representing <c>t1 &gt;= t2</c>
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkInt2Real(Microsoft.Z3.IntExpr)">
             <summary>
             Coerce an integer to a real.
             </summary>
             <remarks>
             There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.
            
             You can take the floor of a real by creating an auxiliary integer Term <c>k</c> and
             and asserting <c>MakeInt2Real(k) &lt;= t1 &lt; MkInt2Real(k)+1</c>.
             The argument must be of integer sort.
             </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkReal2Int(Microsoft.Z3.RealExpr)">
            <summary>
            Coerce a real to an integer.
            </summary>
            <remarks>
            The semantics of this function follows the SMT-LIB standard for the function to_int.
            The argument must be of real sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkIsInteger(Microsoft.Z3.RealExpr)">
            <summary>
            Creates an expression that checks whether a real number is an integer.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVNot(Microsoft.Z3.BitVecExpr)">
            <summary>
            Bitwise negation.
            </summary>
            <remarks>The argument must have a bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVRedAND(Microsoft.Z3.BitVecExpr)">
            <summary>
            Take conjunction of bits in a vector, return vector of length 1.
            </summary>
            <remarks>The argument must have a bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVRedOR(Microsoft.Z3.BitVecExpr)">
            <summary>
            Take disjunction of bits in a vector, return vector of length 1.
            </summary>
            <remarks>The argument must have a bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVAND(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Bitwise conjunction.
            </summary>
            <remarks>The arguments must have a bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVOR(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Bitwise disjunction.
            </summary>
            <remarks>The arguments must have a bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVXOR(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Bitwise XOR.
            </summary>
            <remarks>The arguments must have a bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVNAND(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Bitwise NAND.
            </summary>
            <remarks>The arguments must have a bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVNOR(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Bitwise NOR.
            </summary>
            <remarks>The arguments must have a bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVXNOR(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Bitwise XNOR.
            </summary>
            <remarks>The arguments must have a bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVNeg(Microsoft.Z3.BitVecExpr)">
            <summary>
            Standard two's complement unary minus.
            </summary>
            <remarks>The arguments must have a bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVAdd(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Two's complement addition.
            </summary>
            <remarks>The arguments must have the same bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSub(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Two's complement subtraction.
            </summary>
            <remarks>The arguments must have the same bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVMul(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Two's complement multiplication.
            </summary>
            <remarks>The arguments must have the same bit-vector sort.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVUDiv(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Unsigned division.
            </summary>
            <remarks>
            It is defined as the floor of <c>t1/t2</c> if \c t2 is
            different from zero. If <c>t2</c> is zero, then the result
            is undefined.
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSDiv(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
             <summary>
             Signed division.
             </summary>
             <remarks>
             It is defined in the following way:
            
             - The \c floor of <c>t1/t2</c> if \c t2 is different from zero, and <c>t1*t2 >= 0</c>.
            
             - The \c ceiling of <c>t1/t2</c> if \c t2 is different from zero, and <c>t1*t2 &lt; 0</c>.
                
             If <c>t2</c> is zero, then the result is undefined.
             The arguments must have the same bit-vector sort.
             </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVURem(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Unsigned remainder.
            </summary>
            <remarks>
            It is defined as <c>t1 - (t1 /u t2) * t2</c>, where <c>/u</c> represents unsigned division.       
            If <c>t2</c> is zero, then the result is undefined.
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSRem(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
             <summary>
             Signed remainder.
             </summary>
             <remarks>
             It is defined as <c>t1 - (t1 /s t2) * t2</c>, where <c>/s</c> represents signed division.
             The most significant bit (sign) of the result is equal to the most significant bit of \c t1.
            
             If <c>t2</c> is zero, then the result is undefined.
             The arguments must have the same bit-vector sort.
             </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSMod(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Two's complement signed remainder (sign follows divisor).
            </summary>
            <remarks>
            If <c>t2</c> is zero, then the result is undefined.
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVULT(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Unsigned less-than
            </summary>
            <remarks>    
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSLT(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Two's complement signed less-than
            </summary>
            <remarks>    
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVULE(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Unsigned less-than or equal to.
            </summary>
            <remarks>    
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSLE(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Two's complement signed less-than or equal to.
            </summary>
            <remarks>    
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVUGE(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Unsigned greater than or equal to.
            </summary>
            <remarks>    
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSGE(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
             Two's complement signed greater than or equal to.
            </summary>
            <remarks>    
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVUGT(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Unsigned greater-than.
            </summary>
            <remarks>    
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSGT(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Two's complement signed greater-than.
            </summary>
            <remarks>    
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkConcat(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Bit-vector concatenation.
            </summary>
            <remarks>    
            The arguments must have a bit-vector sort.
            </remarks>
            <returns>
            The result is a bit-vector of size <c>n1+n2</c>, where <c>n1</c> (<c>n2</c>) 
            is the size of <c>t1</c> (<c>t2</c>).
            </returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkExtract(System.UInt32,System.UInt32,Microsoft.Z3.BitVecExpr)">
            <summary>
            Bit-vector extraction.
            </summary>
            <remarks>    
            Extract the bits <paramref name="high"/> down to <paramref name="low"/> from a bitvector of
            size <c>m</c> to yield a new bitvector of size <c>n</c>, where 
            <c>n = high - low + 1</c>.
            The argument <paramref name="t"/> must have a bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSignExt(System.UInt32,Microsoft.Z3.BitVecExpr)">
            <summary>
            Bit-vector sign extension.
            </summary>
            <remarks>    
            Sign-extends the given bit-vector to the (signed) equivalent bitvector of
            size <c>m+i</c>, where \c m is the size of the given bit-vector.
            The argument <paramref name="t"/> must have a bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkZeroExt(System.UInt32,Microsoft.Z3.BitVecExpr)">
            <summary>
            Bit-vector zero extension.
            </summary>
            <remarks>    
            Extend the given bit-vector with zeros to the (unsigned) equivalent
            bitvector of size <c>m+i</c>, where \c m is the size of the
            given bit-vector.
            The argument <paramref name="t"/> must have a bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkRepeat(System.UInt32,Microsoft.Z3.BitVecExpr)">
            <summary>
            Bit-vector repetition.
            </summary>    
            <remarks>
            The argument <paramref name="t"/> must have a bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSHL(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
             <summary>
             Shift left.
             </summary>
             <remarks>
             It is equivalent to multiplication by <c>2^x</c> where \c x is the value of <paramref name="t2"/>.
            
             NB. The semantics of shift operations varies between environments. This 
             definition does not necessarily capture directly the semantics of the 
             programming language or assembly architecture you are modeling.
             
             The arguments must have a bit-vector sort.
             </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVLSHR(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
             <summary>
             Logical shift right
             </summary>
             <remarks>
             It is equivalent to unsigned division by <c>2^x</c> where \c x is the value of <paramref name="t2"/>.
            
             NB. The semantics of shift operations varies between environments. This 
             definition does not necessarily capture directly the semantics of the 
             programming language or assembly architecture you are modeling.
             
             The arguments must have a bit-vector sort.
             </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVASHR(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Arithmetic shift right
            </summary>
            <remarks>
            It is like logical shift right except that the most significant
            bits of the result always copy the most significant bit of the
            second argument.
            
            NB. The semantics of shift operations varies between environments. This 
            definition does not necessarily capture directly the semantics of the 
            programming language or assembly architecture you are modeling.
            
            The arguments must have a bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVRotateLeft(System.UInt32,Microsoft.Z3.BitVecExpr)">
            <summary>
            Rotate Left.
            </summary>
            <remarks>
            Rotate bits of \c t to the left \c i times.
            The argument <paramref name="t"/> must have a bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVRotateRight(System.UInt32,Microsoft.Z3.BitVecExpr)">
            <summary>
            Rotate Right.
            </summary>
            <remarks>
            Rotate bits of \c t to the right \c i times.
            The argument <paramref name="t"/> must have a bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVRotateLeft(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Rotate Left.
            </summary>
            <remarks>
            Rotate bits of <paramref name="t1"/> to the left <paramref name="t2"/> times.
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVRotateRight(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Rotate Right.
            </summary>
            <remarks>
            Rotate bits of <paramref name="t1"/> to the right<paramref name="t2"/> times.
            The arguments must have the same bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkInt2BV(System.UInt32,Microsoft.Z3.IntExpr)">
            <summary>
            Create an <paramref name="n"/> bit bit-vector from the integer argument <paramref name="t"/>.
            </summary>
            <remarks>
            NB. This function is essentially treated as uninterpreted. 
            So you cannot expect Z3 to precisely reflect the semantics of this function
            when solving constraints with this function.
            
            The argument must be of integer sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBV2Int(Microsoft.Z3.BitVecExpr,System.Boolean)">
             <summary>
             Create an integer from the bit-vector argument <paramref name="t"/>.
             </summary>
             <remarks>
             If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned. 
             So the result is non-negative and in the range <c>[0..2^N-1]</c>, where 
             N are the number of bits in <paramref name="t"/>.
             If \c is_signed is true, \c t1 is treated as a signed bit-vector.
            
             NB. This function is essentially treated as uninterpreted. 
             So you cannot expect Z3 to precisely reflect the semantics of this function
             when solving constraints with this function.
             
             The argument must be of bit-vector sort.
             </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVAddNoOverflow(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr,System.Boolean)">
            <summary>
            Create a predicate that checks that the bit-wise addition does not overflow.
            </summary>
            <remarks>
            The arguments must be of bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVAddNoUnderflow(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Create a predicate that checks that the bit-wise addition does not underflow.
            </summary>
            <remarks>
            The arguments must be of bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSubNoOverflow(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Create a predicate that checks that the bit-wise subtraction does not overflow.
            </summary>
            <remarks>
            The arguments must be of bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSubNoUnderflow(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr,System.Boolean)">
            <summary>
            Create a predicate that checks that the bit-wise subtraction does not underflow.
            </summary>
            <remarks>
            The arguments must be of bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVSDivNoOverflow(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Create a predicate that checks that the bit-wise signed division does not overflow.
            </summary>
            <remarks>
            The arguments must be of bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVNegNoOverflow(Microsoft.Z3.BitVecExpr)">
            <summary>
            Create a predicate that checks that the bit-wise negation does not overflow.
            </summary>
            <remarks>
            The arguments must be of bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVMulNoOverflow(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr,System.Boolean)">
            <summary>
            Create a predicate that checks that the bit-wise multiplication does not overflow.
            </summary>
            <remarks>
            The arguments must be of bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBVMulNoUnderflow(Microsoft.Z3.BitVecExpr,Microsoft.Z3.BitVecExpr)">
            <summary>
            Create a predicate that checks that the bit-wise multiplication does not underflow.
            </summary>
            <remarks>
            The arguments must be of bit-vector sort.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkArrayConst(Microsoft.Z3.Symbol,Microsoft.Z3.Sort,Microsoft.Z3.Sort)">
            <summary>
            Create an array constant.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Context.MkArrayConst(System.String,Microsoft.Z3.Sort,Microsoft.Z3.Sort)">
            <summary>
            Create an array constant.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Context.MkSelect(Microsoft.Z3.ArrayExpr,Microsoft.Z3.Expr)">
            <summary>
            Array read.       
            </summary>
            <remarks>
            The argument <c>a</c> is the array and <c>i</c> is the index 
            of the array that gets read.      
            
            The node <c>a</c> must have an array sort <c>[domain -&gt; range]</c>, 
            and <c>i</c> must have the sort <c>domain</c>.
            The sort of the result is <c>range</c>.
            <seealso cref="M:Microsoft.Z3.Context.MkArraySort(Microsoft.Z3.Sort,Microsoft.Z3.Sort)"/>
            <seealso cref="M:Microsoft.Z3.Context.MkStore(Microsoft.Z3.ArrayExpr,Microsoft.Z3.Expr,Microsoft.Z3.Expr)"/>
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkStore(Microsoft.Z3.ArrayExpr,Microsoft.Z3.Expr,Microsoft.Z3.Expr)">
            <summary>
            Array update.       
            </summary>
            <remarks>
            The node <c>a</c> must have an array sort <c>[domain -&gt; range]</c>, 
            <c>i</c> must have sort <c>domain</c>,
            <c>v</c> must have sort range. The sort of the result is <c>[domain -&gt; range]</c>.
            The semantics of this function is given by the theory of arrays described in the SMT-LIB
            standard. See http://smtlib.org for more details.
            The result of this function is an array that is equal to <c>a</c> 
            (with respect to <c>select</c>)
            on all indices except for <c>i</c>, where it maps to <c>v</c> 
            (and the <c>select</c> of <c>a</c> with 
            respect to <c>i</c> may be a different value).
            <seealso cref="M:Microsoft.Z3.Context.MkArraySort(Microsoft.Z3.Sort,Microsoft.Z3.Sort)"/>
            <seealso cref="M:Microsoft.Z3.Context.MkSelect(Microsoft.Z3.ArrayExpr,Microsoft.Z3.Expr)"/>
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkConstArray(Microsoft.Z3.Sort,Microsoft.Z3.Expr)">
            <summary>
            Create a constant array.
            </summary>
            <remarks>
            The resulting term is an array, such that a <c>select</c>on an arbitrary index 
            produces the value <c>v</c>.
            <seealso cref="M:Microsoft.Z3.Context.MkArraySort(Microsoft.Z3.Sort,Microsoft.Z3.Sort)"/>
            <seealso cref="M:Microsoft.Z3.Context.MkSelect(Microsoft.Z3.ArrayExpr,Microsoft.Z3.Expr)"/>
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkMap(Microsoft.Z3.FuncDecl,Microsoft.Z3.ArrayExpr[])">
            <summary>
            Maps f on the argument arrays.
            </summary>
            <remarks>
            Eeach element of <c>args</c> must be of an array sort <c>[domain_i -&gt; range_i]</c>.
            The function declaration <c>f</c> must have type <c> range_1 .. range_n -&gt; range</c>.
            <c>v</c> must have sort range. The sort of the result is <c>[domain_i -&gt; range]</c>.
            <seealso cref="M:Microsoft.Z3.Context.MkArraySort(Microsoft.Z3.Sort,Microsoft.Z3.Sort)"/>
            <seealso cref="M:Microsoft.Z3.Context.MkSelect(Microsoft.Z3.ArrayExpr,Microsoft.Z3.Expr)"/>
            <seealso cref="M:Microsoft.Z3.Context.MkStore(Microsoft.Z3.ArrayExpr,Microsoft.Z3.Expr,Microsoft.Z3.Expr)"/>
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkTermArray(Microsoft.Z3.ArrayExpr)">
            <summary>
            Access the array default value.
            </summary>
            <remarks>
            Produces the default range value, for arrays that can be represented as 
            finite maps with a default range value.    
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSetSort(Microsoft.Z3.Sort)">
            <summary>
            Create a set type.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkEmptySet(Microsoft.Z3.SetSort)">
            <summary>
            Create an empty set.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkFullSet(Microsoft.Z3.SetSort)">
            <summary>
            Create the full set.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSetAdd(Microsoft.Z3.Expr,Microsoft.Z3.Expr)">
            <summary>
            Add an element to the set.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSetDel(Microsoft.Z3.Expr,Microsoft.Z3.Expr)">
            <summary>
            Remove an element from a set.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSetUnion(Microsoft.Z3.Expr[])">
            <summary>
            Take the union of a list of sets.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSetIntersection(Microsoft.Z3.Expr[])">
            <summary>
            Take the intersection of a list of sets.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSetDifference(Microsoft.Z3.Expr,Microsoft.Z3.Expr)">
            <summary>
            Take the difference between two sets.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSetComplement(Microsoft.Z3.Expr)">
            <summary>
            Take the complement of a set.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSetMembership(Microsoft.Z3.Expr,Microsoft.Z3.Expr)">
            <summary>
            Check for set membership.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSetSubset(Microsoft.Z3.Expr,Microsoft.Z3.Expr)">
            <summary>
            Check for subsetness of sets.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkNumeral(System.String,Microsoft.Z3.Sort)">
            <summary>
            Create a Term of a given sort.         
            </summary>
            <param name="v">A string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form <c>[num]* / [num]*</c>.</param>
            <param name="ty">The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size. </param>
            <returns>A Term with value <paramref name="v"/> and sort <paramref name="ty"/> </returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkNumeral(System.Int32,Microsoft.Z3.Sort)">
            <summary>
            Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
            It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.       
            </summary>
            <param name="v">Value of the numeral</param>
            <param name="ty">Sort of the numeral</param>
            <returns>A Term with value <paramref name="v"/> and type <paramref name="ty"/></returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkNumeral(System.UInt32,Microsoft.Z3.Sort)">
            <summary>
            Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
            It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.       
            </summary>
            <param name="v">Value of the numeral</param>
            <param name="ty">Sort of the numeral</param>
            <returns>A Term with value <paramref name="v"/> and type <paramref name="ty"/></returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkNumeral(System.Int64,Microsoft.Z3.Sort)">
            <summary>
            Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
            It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.       
            </summary>
            <param name="v">Value of the numeral</param>
            <param name="ty">Sort of the numeral</param>
            <returns>A Term with value <paramref name="v"/> and type <paramref name="ty"/></returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkNumeral(System.UInt64,Microsoft.Z3.Sort)">
            <summary>
            Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
            It is slightly faster than <c>MakeNumeral</c> since it is not necessary to parse a string.       
            </summary>
            <param name="v">Value of the numeral</param>
            <param name="ty">Sort of the numeral</param>
            <returns>A Term with value <paramref name="v"/> and type <paramref name="ty"/></returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkReal(System.Int32,System.Int32)">
            <summary>
            Create a real from a fraction.
            </summary>
            <param name="num">numerator of rational.</param>
            <param name="den">denominator of rational.</param>
            <returns>A Term with value <paramref name="num"/>/<paramref name="den"/> and sort Real</returns>
            <seealso cref="M:Microsoft.Z3.Context.MkNumeral(System.String,Microsoft.Z3.Sort)"/>
        </member>
        <member name="M:Microsoft.Z3.Context.MkReal(System.String)">
            <summary>
            Create a real numeral.
            </summary>
            <param name="v">A string representing the Term value in decimal notation.</param>
            <returns>A Term with value <paramref name="v"/> and sort Real</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkReal(System.Int32)">
            <summary>
            Create a real numeral.
            </summary>
            <param name="v">value of the numeral.</param>    
            <returns>A Term with value <paramref name="v"/> and sort Real</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkReal(System.UInt32)">
            <summary>
            Create a real numeral.
            </summary>
            <param name="v">value of the numeral.</param>    
            <returns>A Term with value <paramref name="v"/> and sort Real</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkReal(System.Int64)">
            <summary>
            Create a real numeral.
            </summary>
            <param name="v">value of the numeral.</param>    
            <returns>A Term with value <paramref name="v"/> and sort Real</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkReal(System.UInt64)">
            <summary>
            Create a real numeral.
            </summary>
            <param name="v">value of the numeral.</param>    
            <returns>A Term with value <paramref name="v"/> and sort Real</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkInt(System.String)">
            <summary>
            Create an integer numeral.
            </summary>
            <param name="v">A string representing the Term value in decimal notation.</param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkInt(System.Int32)">
            <summary>
            Create an integer numeral.
            </summary>
            <param name="v">value of the numeral.</param>    
            <returns>A Term with value <paramref name="v"/> and sort Integer</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkInt(System.UInt32)">
            <summary>
            Create an integer numeral.
            </summary>
            <param name="v">value of the numeral.</param>    
            <returns>A Term with value <paramref name="v"/> and sort Integer</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkInt(System.Int64)">
            <summary>
            Create an integer numeral.
            </summary>
            <param name="v">value of the numeral.</param>    
            <returns>A Term with value <paramref name="v"/> and sort Integer</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkInt(System.UInt64)">
            <summary>
            Create an integer numeral.
            </summary>
            <param name="v">value of the numeral.</param>    
            <returns>A Term with value <paramref name="v"/> and sort Integer</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBV(System.String,System.UInt32)">
            <summary>
            Create a bit-vector numeral.
            </summary>
            <param name="v">A string representing the value in decimal notation.</param>
            <param name="size">the size of the bit-vector</param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBV(System.Int32,System.UInt32)">
            <summary>
            Create a bit-vector numeral.
            </summary>
            <param name="v">value of the numeral.</param>    
            <param name="size">the size of the bit-vector</param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBV(System.UInt32,System.UInt32)">
            <summary>
            Create a bit-vector numeral.
            </summary>
            <param name="v">value of the numeral.</param>    
            <param name="size">the size of the bit-vector</param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBV(System.Int64,System.UInt32)">
            <summary>
            Create a bit-vector numeral.
            </summary>
            <param name="v">value of the numeral.</param>
            /// <param name="size">the size of the bit-vector</param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkBV(System.UInt64,System.UInt32)">
            <summary>
            Create a bit-vector numeral.
            </summary>
            <param name="v">value of the numeral.</param>
            <param name="size">the size of the bit-vector</param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkForall(Microsoft.Z3.Sort[],Microsoft.Z3.Symbol[],Microsoft.Z3.Expr,System.UInt32,Microsoft.Z3.Pattern[],Microsoft.Z3.Expr[],Microsoft.Z3.Symbol,Microsoft.Z3.Symbol)">
            <summary>
            Create a universal Quantifier.
            </summary>
            <remarks>
            Creates a forall formula, where <paramref name="weight"/> is the weight, 
            <paramref name="patterns"/> is an array of patterns, <paramref name="sorts"/> is an array
            with the sorts of the bound variables, <paramref name="names"/> is an array with the
            'names' of the bound variables, and <paramref name="body"/> is the body of the
            quantifier. Quantifiers are associated with weights indicating
            the importance of using the quantifier during instantiation. 
            </remarks>
            <param name="sorts">the sorts of the bound variables.</param>
            <param name="names">names of the bound variables</param>
            <param name="body">the body of the quantifier.</param>
            <param name="weight">quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.</param>
            <param name="patterns">array containing the patterns created using <c>MkPattern</c>.</param>
            <param name="noPatterns">array containing the anti-patterns created using <c>MkPattern</c>.</param>
            <param name="quantifierID">optional symbol to track quantifier.</param>
            <param name="skolemID">optional symbol to track skolem constants.</param>
        </member>
        <member name="M:Microsoft.Z3.Context.MkForall(Microsoft.Z3.Expr[],Microsoft.Z3.Expr,System.UInt32,Microsoft.Z3.Pattern[],Microsoft.Z3.Expr[],Microsoft.Z3.Symbol,Microsoft.Z3.Symbol)">
            <summary>
            Create a universal Quantifier.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkExists(Microsoft.Z3.Sort[],Microsoft.Z3.Symbol[],Microsoft.Z3.Expr,System.UInt32,Microsoft.Z3.Pattern[],Microsoft.Z3.Expr[],Microsoft.Z3.Symbol,Microsoft.Z3.Symbol)">
            <summary>
            Create an existential Quantifier.
            </summary>
            <seealso cref="M:Microsoft.Z3.Context.MkForall(Microsoft.Z3.Sort[],Microsoft.Z3.Symbol[],Microsoft.Z3.Expr,System.UInt32,Microsoft.Z3.Pattern[],Microsoft.Z3.Expr[],Microsoft.Z3.Symbol,Microsoft.Z3.Symbol)"/>
        </member>
        <member name="M:Microsoft.Z3.Context.MkExists(Microsoft.Z3.Expr[],Microsoft.Z3.Expr,System.UInt32,Microsoft.Z3.Pattern[],Microsoft.Z3.Expr[],Microsoft.Z3.Symbol,Microsoft.Z3.Symbol)">
            <summary>
            Create an existential Quantifier.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkQuantifier(System.Boolean,Microsoft.Z3.Sort[],Microsoft.Z3.Symbol[],Microsoft.Z3.Expr,System.UInt32,Microsoft.Z3.Pattern[],Microsoft.Z3.Expr[],Microsoft.Z3.Symbol,Microsoft.Z3.Symbol)">
            <summary>
            Create a Quantifier.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkQuantifier(System.Boolean,Microsoft.Z3.Expr[],Microsoft.Z3.Expr,System.UInt32,Microsoft.Z3.Pattern[],Microsoft.Z3.Expr[],Microsoft.Z3.Symbol,Microsoft.Z3.Symbol)">
            <summary>
            Create a Quantifier.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.BenchmarkToSMTString(System.String,System.String,System.String,System.String,Microsoft.Z3.BoolExpr[],Microsoft.Z3.BoolExpr)">
            <summary>
            Convert a benchmark into an SMT-LIB formatted string.
            </summary>
            <param name="name">Name of the benchmark. The argument is optional.</param>
            <param name="logic">The benchmark logic. </param>
            <param name="status">The status string (sat, unsat, or unknown)</param>
            <param name="attributes">Other attributes, such as source, difficulty or category.</param>
            <param name="assumptions">Auxiliary assumptions.</param>
            <param name="formula">Formula to be checked for consistency in conjunction with assumptions.</param>
            <returns>A string representation of the benchmark.</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.ParseSMTLIBString(System.String,Microsoft.Z3.Symbol[],Microsoft.Z3.Sort[],Microsoft.Z3.Symbol[],Microsoft.Z3.FuncDecl[])">
            <summary>
            Parse the given string using the SMT-LIB parser. 
            </summary>
            <remarks>
            The symbol table of the parser can be initialized using the given sorts and declarations. 
            The symbols in the arrays <paramref name="sortNames"/> and <paramref name="declNames"/> 
            don't need to match the names of the sorts and declarations in the arrays <paramref name="sorts"/> 
            and <paramref name="decls"/>. This is a useful feature since we can use arbitrary names to 
            reference sorts and declarations.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.ParseSMTLIBFile(System.String,Microsoft.Z3.Symbol[],Microsoft.Z3.Sort[],Microsoft.Z3.Symbol[],Microsoft.Z3.FuncDecl[])">
            <summary>
            Parse the given file using the SMT-LIB parser. 
            </summary>
            <seealso cref="M:Microsoft.Z3.Context.ParseSMTLIBString(System.String,Microsoft.Z3.Symbol[],Microsoft.Z3.Sort[],Microsoft.Z3.Symbol[],Microsoft.Z3.FuncDecl[])"/>
        </member>
        <member name="M:Microsoft.Z3.Context.ParseSMTLIB2String(System.String,Microsoft.Z3.Symbol[],Microsoft.Z3.Sort[],Microsoft.Z3.Symbol[],Microsoft.Z3.FuncDecl[])">
            <summary>
            Parse the given string using the SMT-LIB2 parser. 
            </summary>
            <seealso cref="M:Microsoft.Z3.Context.ParseSMTLIBString(System.String,Microsoft.Z3.Symbol[],Microsoft.Z3.Sort[],Microsoft.Z3.Symbol[],Microsoft.Z3.FuncDecl[])"/>
            <returns>A conjunction of assertions in the scope (up to push/pop) at the end of the string.</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.ParseSMTLIB2File(System.String,Microsoft.Z3.Symbol[],Microsoft.Z3.Sort[],Microsoft.Z3.Symbol[],Microsoft.Z3.FuncDecl[])">
            <summary>
            Parse the given file using the SMT-LIB2 parser. 
            </summary>
            <seealso cref="M:Microsoft.Z3.Context.ParseSMTLIB2String(System.String,Microsoft.Z3.Symbol[],Microsoft.Z3.Sort[],Microsoft.Z3.Symbol[],Microsoft.Z3.FuncDecl[])"/>
        </member>
        <member name="M:Microsoft.Z3.Context.ParseZ3String(System.String)">
            <summary>
            Parse the given string using the Z3 native parser.            
            </summary>    
            <returns>A conjunction of asserts made in <paramref name="str"/>.</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.ParseZ3File(System.String)">
            <summary>
            Parse the given file using the Z3 native parser.            
            </summary>    
            <returns>A conjunction of asserts made in the file.</returns>
        </member>
        <member name="M:Microsoft.Z3.Context.MkGoal(System.Boolean,System.Boolean,System.Boolean)">
            <summary>
            Creates a new Goal.
            </summary>
            <remarks>
            Note that the Context must have been created with proof generation support if 
            <paramref name="proofs"/> is set to true here.
            </remarks>
            <param name="models">Indicates whether model generation should be enabled.</param>
            <param name="unsatCores">Indicates whether unsat core generation should be enabled.</param>
            <param name="proofs">Indicates whether proof generation should be enabled.</param>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkParams">
            <summary>
            Creates a new ParameterSet.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.TacticDescription(System.String)">
            <summary>
            Returns a string containing a description of the tactic with the given name.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkTactic(System.String)">
            <summary>
            Creates a new Tactic.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.AndThen(Microsoft.Z3.Tactic,Microsoft.Z3.Tactic,Microsoft.Z3.Tactic[])">
            <summary>
            Create a tactic that applies <paramref name="t1"/> to a Goal and
            then <paramref name="t2"/> to every subgoal produced by <paramref name="t1"/>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Then(Microsoft.Z3.Tactic,Microsoft.Z3.Tactic,Microsoft.Z3.Tactic[])">
            <summary>
            Create a tactic that applies <paramref name="t1"/> to a Goal and
            then <paramref name="t2"/> to every subgoal produced by <paramref name="t1"/>.        
            </summary>
            <remarks>
            Shorthand for <c>AndThen</c>.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.OrElse(Microsoft.Z3.Tactic,Microsoft.Z3.Tactic)">
            <summary>
            Create a tactic that first applies <paramref name="t1"/> to a Goal and
            if it fails then returns the result of <paramref name="t2"/> applied to the Goal.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.TryFor(Microsoft.Z3.Tactic,System.UInt32)">
            <summary>
            Create a tactic that applies <paramref name="t"/> to a goal for <paramref name="ms"/> milliseconds.    
            </summary>
            <remarks>
            If <paramref name="t"/> does not terminate within <paramref name="ms"/> milliseconds, then it fails.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.When(Microsoft.Z3.Probe,Microsoft.Z3.Tactic)">
            <summary>
            Create a tactic that applies <paramref name="t"/> to a given goal if the probe 
            <paramref name="p"/> evaluates to true. 
            </summary>
            <remarks>
            If <paramref name="p"/> evaluates to false, then the new tactic behaves like the <c>skip</c> tactic. 
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.Cond(Microsoft.Z3.Probe,Microsoft.Z3.Tactic,Microsoft.Z3.Tactic)">
            <summary>
            Create a tactic that applies <paramref name="t1"/> to a given goal if the probe 
            <paramref name="p"/> evaluates to true and <paramref name="t2"/> otherwise.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Repeat(Microsoft.Z3.Tactic,System.UInt32)">
            <summary>
            Create a tactic that keeps applying <paramref name="t"/> until the goal is not 
            modified anymore or the maximum number of iterations <paramref name="max"/> is reached.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Skip">
            <summary>
            Create a tactic that just returns the given goal.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Fail">
            <summary>
            Create a tactic always fails.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.FailIf(Microsoft.Z3.Probe)">
            <summary>
            Create a tactic that fails if the probe <paramref name="p"/> evaluates to false.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.FailIfNotDecided">
            <summary>
            Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty)
            or trivially unsatisfiable (i.e., contains `false').
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.UsingParams(Microsoft.Z3.Tactic,Microsoft.Z3.Params)">
            <summary>
            Create a tactic that applies <paramref name="t"/> using the given set of parameters <paramref name="p"/>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.With(Microsoft.Z3.Tactic,Microsoft.Z3.Params)">
            <summary>
            Create a tactic that applies <paramref name="t"/> using the given set of parameters <paramref name="p"/>.
            </summary>
            <remarks>Alias for <c>UsingParams</c></remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.ParOr(Microsoft.Z3.Tactic[])">
            <summary>
            Create a tactic that applies the given tactics in parallel.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.ParAndThen(Microsoft.Z3.Tactic,Microsoft.Z3.Tactic)">
            <summary>
            Create a tactic that applies <paramref name="t1"/> to a given goal and then <paramref name="t2"/>
            to every subgoal produced by <paramref name="t1"/>. The subgoals are processed in parallel.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Interrupt">
            <summary>
            Interrupt the execution of a Z3 procedure.        
            </summary>
            <remarks>This procedure can be used to interrupt: solvers, simplifiers and tactics.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.ProbeDescription(System.String)">
            <summary>
            Returns a string containing a description of the probe with the given name.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkProbe(System.String)">
            <summary>
            Creates a new Probe.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Context.Const(System.Double)">
            <summary>
            Create a probe that always evaluates to <paramref name="val"/>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Lt(Microsoft.Z3.Probe,Microsoft.Z3.Probe)">
            <summary>
            Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
            is less than the value returned by <paramref name="p2"/>
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Gt(Microsoft.Z3.Probe,Microsoft.Z3.Probe)">
            <summary>
            Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
            is greater than the value returned by <paramref name="p2"/>
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Le(Microsoft.Z3.Probe,Microsoft.Z3.Probe)">
            <summary>
            Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
            is less than or equal the value returned by <paramref name="p2"/>
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Ge(Microsoft.Z3.Probe,Microsoft.Z3.Probe)">
            <summary>
            Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
            is greater than or equal the value returned by <paramref name="p2"/>
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Eq(Microsoft.Z3.Probe,Microsoft.Z3.Probe)">
            <summary>
            Create a probe that evaluates to "true" when the value returned by <paramref name="p1"/>
            is equal to the value returned by <paramref name="p2"/>
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.And(Microsoft.Z3.Probe,Microsoft.Z3.Probe)">
            <summary>
            Create a probe that evaluates to "true" when the value <paramref name="p1"/>
            and <paramref name="p2"/> evaluate to "true".
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Or(Microsoft.Z3.Probe,Microsoft.Z3.Probe)">
            <summary>
            Create a probe that evaluates to "true" when the value <paramref name="p1"/>
            or <paramref name="p2"/> evaluate to "true".
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Not(Microsoft.Z3.Probe)">
            <summary>
            Create a probe that evaluates to "true" when the value <paramref name="p"/>
            does not evaluate to "true".
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSolver(Microsoft.Z3.Symbol)">
            <summary>
            Creates a new (incremental) solver. 
            </summary>
            <remarks>
            This solver also uses a set of builtin tactics for handling the first 
            check-sat command, and check-sat commands that take more than a given 
            number of milliseconds to be solved. 
            </remarks>    
        </member>
        <member name="M:Microsoft.Z3.Context.MkSolver(System.String)">
            <summary>
            Creates a new (incremental) solver.
            </summary>        
            <seealso cref="M:Microsoft.Z3.Context.MkSolver(Microsoft.Z3.Symbol)"/>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSimpleSolver">
            <summary>
            Creates a new (incremental) solver. 
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.MkSolver(Microsoft.Z3.Tactic)">
            <summary>
            Creates a solver that is implemented using the given tactic.
            </summary>
            <remarks>
            The solver supports the commands <c>Push</c> and <c>Pop</c>, but it
            will always solve each check from scratch.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.MkFixedpoint">
            <summary>
            Create a Fixedpoint context.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.SimplifyHelp">
            <summary>
            Return a string describing all available parameters to <c>Expr.Simplify</c>.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.ToggleWarningMessages(System.Boolean)">
            <summary>
            Enable/disable printing of warning messages to the console.
            </summary>
            <remarks>Note that this function is static and effects the behaviour of 
            all contexts globally.</remarks>
        </member>
        <member name="M:Microsoft.Z3.Context.UpdateParamValue(System.String,System.String)">
            <summary>
            Update a mutable configuration parameter.
            </summary>
            <remarks>
            The list of all configuration parameters can be obtained using the Z3 executable:
            <c>z3.exe -ini?</c>
            Only a few configuration parameters are mutable once the context is created.
            An exception is thrown when trying to modify an immutable parameter.
            </remarks>
            <seealso cref="M:Microsoft.Z3.Context.GetParamValue(System.String)"/>
        </member>
        <member name="M:Microsoft.Z3.Context.GetParamValue(System.String)">
            <summary>
            Get a configuration parameter.
            </summary>
            <remarks>
            Returns null if the parameter value does not exist.
            </remarks>
            <seealso cref="M:Microsoft.Z3.Context.UpdateParamValue(System.String,System.String)"/>
        </member>
        <member name="M:Microsoft.Z3.Context.Finalize">
            <summary>
            Finalizer.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Context.Dispose">
            <summary>
            Disposes of the context.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.BoolSort">
            <summary>
            Retrieves the Boolean sort of the context.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.IntSort">
            <summary>
            Retrieves the Integer sort of the context.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.RealSort">
            <summary>
            Retrieves the Real sort of the context.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.PrintMode">
            <summary>
            Selects the format used for pretty-printing expressions.
            </summary>
            <remarks>
            The default mode for pretty printing expressions is to produce
            SMT-LIB style output where common subexpressions are printed 
            at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL.
            To print shared common subexpressions only once, 
            use the Z3_PRINT_LOW_LEVEL mode.
            To print in way that conforms to SMT-LIB standards and uses let
            expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.
            </remarks>
            <seealso cref="M:Microsoft.Z3.AST.ToString"/>
            <seealso cref="M:Microsoft.Z3.Pattern.ToString"/>
            <seealso cref="M:Microsoft.Z3.FuncDecl.ToString"/>
            <seealso cref="M:Microsoft.Z3.Sort.ToString"/>
        </member>
        <member name="P:Microsoft.Z3.Context.NumSMTLIBFormulas">
            <summary>
            The number of SMTLIB formulas parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.SMTLIBFormulas">
            <summary>
            The formulas parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.NumSMTLIBAssumptions">
            <summary>
            The number of SMTLIB assumptions parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.SMTLIBAssumptions">
            <summary>
            The assumptions parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.NumSMTLIBDecls">
            <summary>
            The number of SMTLIB declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.SMTLIBDecls">
            <summary>
            The declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.NumSMTLIBSorts">
            <summary>
            The number of SMTLIB sorts parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.SMTLIBSorts">
            <summary>
            The declarations parsed by the last call to <c>ParseSMTLIBString</c> or <c>ParseSMTLIBFile</c>.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.NumTactics">
            <summary>
            The number of supported tactics.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.TacticNames">
            <summary>
            The names of all supported tactics.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.NumProbes">
            <summary>
            The number of supported Probes.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Context.ProbeNames">
            <summary>
            The names of all supported Probes.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Z3_lbool">
            <summary>Z3_lbool</summary>
        </member>
        <member name="T:Microsoft.Z3.Z3_symbol_kind">
            <summary>Z3_symbol_kind</summary>
        </member>
        <member name="T:Microsoft.Z3.Z3_parameter_kind">
            <summary>Z3_parameter_kind</summary>
        </member>
        <member name="T:Microsoft.Z3.Z3_sort_kind">
            <summary>Z3_sort_kind</summary>
        </member>
        <member name="T:Microsoft.Z3.Z3_ast_kind">
            <summary>Z3_ast_kind</summary>
        </member>
        <member name="T:Microsoft.Z3.Z3_decl_kind">
            <summary>Z3_decl_kind</summary>
        </member>
        <member name="T:Microsoft.Z3.Z3_ast_print_mode">
            <summary>Z3_ast_print_mode</summary>
        </member>
        <member name="T:Microsoft.Z3.Z3_error_code">
            <summary>Z3_error_code</summary>
        </member>
        <member name="T:Microsoft.Z3.Z3_goal_prec">
            <summary>Z3_goal_prec</summary>
        </member>
        <member name="T:Microsoft.Z3.Constructor">
            <summary>
            Constructors are used for datatype sorts.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Constructor.Finalize">
            <summary>
            Destructor.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Constructor.NumFields">
            <summary>
            The number of fields of the constructor.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Constructor.ConstructorDecl">
            <summary>
            The function declaration of the constructor.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Constructor.TesterDecl">
            <summary>
            The function declaration of the tester.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Constructor.AccessorDecls">
            <summary>
            The function declarations of the accessors
            </summary>
        </member>
        <member name="T:Microsoft.Z3.ConstructorList">
            <summary>
            Lists of constructors
            </summary>
        </member>
        <member name="M:Microsoft.Z3.ConstructorList.Finalize">
            <summary>
            Destructor.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.ApplyResult">
            <summary>
            ApplyResult objects represent the result of an application of a 
            tactic to a goal. It contains the subgoals that were produced.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.ApplyResult.ConvertModel(System.UInt32,Microsoft.Z3.Model)">
            <summary>
            Convert a model for the subgoal <paramref name="i"/> into a model for the original 
            goal <c>g</c>, that the ApplyResult was obtained from. 
            </summary>
            <returns>A model for <c>g</c></returns>
        </member>
        <member name="M:Microsoft.Z3.ApplyResult.ToString">
            <summary>
            A string representation of the ApplyResult.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ApplyResult.NumSubgoals">
            <summary>
            The number of Subgoals.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.ApplyResult.Subgoals">
            <summary>
            Retrieves the subgoals from the ApplyResult.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Status">
            <summary>
            Status values.
            </summary>
        </member>
        <member name="F:Microsoft.Z3.Status.UNSATISFIABLE">
            <summary>
            Used to signify an unsatisfiable status.
            </summary>
        </member>
        <member name="F:Microsoft.Z3.Status.UNKNOWN">
            <summary>
            Used to signify an unknown status.
            </summary>
        </member>
        <member name="F:Microsoft.Z3.Status.SATISFIABLE">
            <summary>
            Used to signify a satisfiable status.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Probe">
            <summary>  
            Probes are used to inspect a goal (aka problem) and collect information that may be used to decide
            which solver and/or preprocessing step will be used.
            The complete list of probes may be obtained using the procedures <c>Context.NumProbes</c>
            and <c>Context.ProbeNames</c>.
            It may also be obtained using the command <c>(help-tactics)</c> in the SMT 2.0 front-end.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Probe.Apply(Microsoft.Z3.Goal)">
            <summary>
            Execute the probe over the goal. 
            </summary>
            <returns>A probe always produce a double value.
            "Boolean" probes return 0.0 for false, and a value different from 0.0 for true.</returns>
        </member>
        <member name="P:Microsoft.Z3.Probe.Item(Microsoft.Z3.Goal)">
            <summary>
            Apply the probe to a goal.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.Statistics">
            <summary>
            Objects of this class track statistical information about solvers. 
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Statistics.ToString">
            <summary>
            A string representation of the statistical data.
            </summary>    
        </member>
        <member name="P:Microsoft.Z3.Statistics.Size">
            <summary>
            The number of statistical data.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Statistics.Entries">
            <summary>
            The data entries.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Statistics.Keys">
            <summary>
            The statistical counters.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Statistics.Item(System.String)">
            <summary>
            The value of a particular statistical counter.
            </summary>        
            <remarks>Returns null if the key is unknown.</remarks>
        </member>
        <member name="T:Microsoft.Z3.Statistics.Entry">
            <summary>
            Statistical data is organized into pairs of [Key, Entry], where every
            Entry is either a <c>DoubleEntry</c> or a <c>UIntEntry</c>
            </summary>
        </member>
        <member name="F:Microsoft.Z3.Statistics.Entry.Key">
            <summary>
            The key of the entry.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Statistics.Entry.ToString">
            <summary>
            The string representation of the Entry.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Statistics.Entry.UIntValue">
            <summary>
            The uint-value of the entry.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Statistics.Entry.DoubleValue">
            <summary>
            The double-value of the entry.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Statistics.Entry.IsUInt">
            <summary>
            True if the entry is uint-valued.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Statistics.Entry.IsDouble">
            <summary>
            True if the entry is double-valued.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.Statistics.Entry.Value">
            <summary>
            The string representation of the the entry's value.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.IntNum">
            <summary>
            Integer Numerals
            </summary>
        </member>
        <member name="M:Microsoft.Z3.IntNum.ToString">
            <summary>
            Returns a string representation of the numeral.
            </summary>        
        </member>
        <member name="P:Microsoft.Z3.IntNum.UInt64">
            <summary>
            Retrieve the 64-bit unsigned integer value.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.IntNum.Int">
            <summary>
            Retrieve the int value.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.IntNum.Int64">
            <summary>
            Retrieve the 64-bit int value.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.IntNum.UInt">
            <summary>
            Retrieve the int value.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.IntNum.BigInteger">
            <summary>
            Retrieve the BigInteger value.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.RatNum">
            <summary>
            Rational Numerals
            </summary>
        </member>
        <member name="M:Microsoft.Z3.RatNum.ToDecimalString(System.UInt32)">
            <summary>
            Returns a string representation in decimal notation.
            </summary>
            <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>    
        </member>
        <member name="M:Microsoft.Z3.RatNum.ToString">
            <summary>
            Returns a string representation of the numeral.
            </summary>        
        </member>
        <member name="P:Microsoft.Z3.RatNum.Numerator">
            <summary>
            The numerator of a rational numeral.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.RatNum.Denominator">
            <summary>
            The denominator of a rational numeral.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.RatNum.BigIntNumerator">
            <summary>
            Converts the numerator of the rational to a BigInteger
            </summary>
        </member>
        <member name="P:Microsoft.Z3.RatNum.BigIntDenominator">
            <summary>
            Converts the denominator of the rational to a BigInteger
            </summary>
        </member>
        <member name="T:Microsoft.Z3.BitVecNum">
            <summary>
            Bit-vector numerals
            </summary>
        </member>
        <member name="M:Microsoft.Z3.BitVecNum.ToString">
            <summary>
            Returns a string representation of the numeral.
            </summary>        
        </member>
        <member name="P:Microsoft.Z3.BitVecNum.UInt64">
            <summary>
            Retrieve the 64-bit unsigned integer value.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.BitVecNum.Int">
            <summary>
            Retrieve the int value.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.BitVecNum.Int64">
            <summary>
            Retrieve the 64-bit int value.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.BitVecNum.UInt">
            <summary>
            Retrieve the int value.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.BitVecNum.BigInteger">
            <summary>
            Retrieve the BigInteger value.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.AlgebraicNum">
            <summary>
            Algebraic numbers
            </summary>
        </member>
        <member name="M:Microsoft.Z3.AlgebraicNum.ToUpper(System.UInt32)">
            <summary>
            Return a upper bound for a given real algebraic number. 
            The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.    
            <seealso cref="P:Microsoft.Z3.Expr.IsAlgebraicNumber"/>   
            </summary>
            <param name="precision">the precision of the result</param>
            <returns>A numeral Expr of sort Real</returns>
        </member>
        <member name="M:Microsoft.Z3.AlgebraicNum.ToLower(System.UInt32)">
            <summary>
            Return a lower bound for the given real algebraic number. 
            The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.    
            <seealso cref="P:Microsoft.Z3.Expr.IsAlgebraicNumber"/>
            </summary>
            <param name="precision"></param>
            <returns>A numeral Expr of sort Real</returns>
        </member>
        <member name="M:Microsoft.Z3.AlgebraicNum.ToDecimal(System.UInt32)">
            <summary>
            Returns a string representation in decimal notation.
            </summary>
            <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>    
        </member>
        <member name="T:Microsoft.Z3.Fixedpoint">
            <summary>
            Object for managing fixedpoints
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Fixedpoint.Assert(Microsoft.Z3.BoolExpr[])">
            <summary>
            Assert a constraint (or multiple) into the fixedpoint solver.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Fixedpoint.RegisterRelation(Microsoft.Z3.FuncDecl)">
            <summary>
            Register predicate as recursive relation.
            </summary>       
        </member>
        <member name="M:Microsoft.Z3.Fixedpoint.AddRule(Microsoft.Z3.BoolExpr,Microsoft.Z3.Symbol)">
            <summary>
            Add rule into the fixedpoint solver.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Fixedpoint.AddFact(Microsoft.Z3.FuncDecl,System.UInt32[])">
            <summary>
            Add table fact to the fixedpoint solver.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Fixedpoint.Query(Microsoft.Z3.BoolExpr)">
            <summary>
            Query the fixedpoint solver.
            A query is a conjunction of constraints. The constraints may include the recursively defined relations.
            The query is satisfiable if there is an instance of the query variables and a derivation for it.
            The query is unsatisfiable if there are no derivations satisfying the query variables. 
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Fixedpoint.Query(Microsoft.Z3.FuncDecl[])">
            <summary>
            Query the fixedpoint solver.
            A query is an array of relations.
            The query is satisfiable if there is an instance of some relation that is non-empty.
            The query is unsatisfiable if there are no derivations satisfying any of the relations.
            </summary>        
        </member>
        <member name="M:Microsoft.Z3.Fixedpoint.GetAnswer">
            <summary>
            Retrieve satisfying instance or instances of solver, 
            or definitions for the recursive predicates that show unsatisfiability.
            </summary>                
        </member>
        <member name="M:Microsoft.Z3.Fixedpoint.GetReasonUnknown">
            <summary>
            Retrieve explanation why fixedpoint engine returned status Unknown.
            </summary>                
        </member>
        <member name="M:Microsoft.Z3.Fixedpoint.ToString">
            <summary>
            Retrieve internal string representation of fixedpoint object.
            </summary>                
        </member>
        <member name="M:Microsoft.Z3.Fixedpoint.SetPredicateRepresentation(Microsoft.Z3.FuncDecl,Microsoft.Z3.Symbol[])">
            <summary>
            Instrument the Datalog engine on which table representation to use for recursive predicate.
            </summary>                
        </member>
        <member name="M:Microsoft.Z3.Fixedpoint.ToString(Microsoft.Z3.BoolExpr[])">
            <summary>
            Convert benchmark given as set of axioms, rules and queries to a string.
            </summary>                
        </member>
        <member name="T:Microsoft.Z3.Log">
            <summary>
            Interaction logging for Z3.
            </summary>
            <remarks>
            Note that this is a global, static log and if multiple Context 
            objects are created, it logs the interaction with all of them.
            </remarks>
        </member>
        <member name="M:Microsoft.Z3.Log.Open(System.String)">
            <summary>
            Open an interaction log file.
            </summary>
            <param name="filename">the name of the file to open</param>
            <returns>True if opening the log file succeeds, false otherwise.</returns>
        </member>
        <member name="M:Microsoft.Z3.Log.Close">
            <summary>
            Closes the interaction log.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Log.Append(System.String)">
            <summary>
            Appends the user-provided string <paramref name="s"/> to the interaction log.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.Log.isOpen">
            <summary>
            Checks whether the interaction log is opened.
            </summary>
            <returns>True if the interaction log is open, false otherwise.</returns>
        </member>
        <member name="T:Microsoft.Z3.Params">
            <summary>
            A ParameterSet represents a configuration in the form of Symbol/value pairs.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Params.Add(Microsoft.Z3.Symbol,System.Boolean)">
            <summary>
            Adds a parameter setting.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Params.Add(Microsoft.Z3.Symbol,System.UInt32)">
            <summary>
            Adds a parameter setting.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Params.Add(Microsoft.Z3.Symbol,System.Double)">
            <summary>
            Adds a parameter setting.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Params.Add(Microsoft.Z3.Symbol,Microsoft.Z3.Symbol)">
            <summary>
            Adds a parameter setting.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Params.Add(System.String,System.Boolean)">
            <summary>
            Adds a parameter setting.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Params.Add(System.String,System.UInt32)">
            <summary>
            Adds a parameter setting.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Params.Add(System.String,System.Double)">
            <summary>
            Adds a parameter setting.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Params.Add(System.String,Microsoft.Z3.Symbol)">
            <summary>
            Adds a parameter setting.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.Params.ToString">
            <summary>
            A string representation of the parameter set.
            </summary>
        </member>
        <member name="T:Microsoft.Z3.FuncDecl">
            <summary>
            Function declarations. 
            </summary>
        </member>
        <member name="M:Microsoft.Z3.FuncDecl.op_Equality(Microsoft.Z3.FuncDecl,Microsoft.Z3.FuncDecl)">
            <summary>
            Comparison operator.
            </summary>
            <returns>True if <paramref name="a"/> and <paramref name="b"/> share the same context and are equal, false otherwise.</returns>
        </member>
        <member name="M:Microsoft.Z3.FuncDecl.op_Inequality(Microsoft.Z3.FuncDecl,Microsoft.Z3.FuncDecl)">
            <summary>
            Comparison operator.
            </summary>
            <returns>True if <paramref name="a"/> and <paramref name="b"/> do not share the same context or are not equal, false otherwise.</returns>
        </member>
        <member name="M:Microsoft.Z3.FuncDecl.Equals(System.Object)">
            <summary>
            Object comparison.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.FuncDecl.GetHashCode">
            <summary>
            A hash code.
            </summary>    
        </member>
        <member name="M:Microsoft.Z3.FuncDecl.ToString">
            <summary>
            A string representations of the function declaration.
            </summary>
        </member>
        <member name="M:Microsoft.Z3.FuncDecl.Apply(Microsoft.Z3.Expr[])">
            <summary>
            Create expression that applies function to arguments.
            </summary>
            <param name="args"></param>
            <returns></returns>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Id">
            <summary>
            Returns a unique identifier for the function declaration.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Arity">
            <summary>
            The arity of the function declaration
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.DomainSize">
            <summary>
            The size of the domain of the function declaration
            <seealso cref="P:Microsoft.Z3.FuncDecl.Arity"/>
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Domain">
            <summary>
            The domain of the function declaration
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Range">
            <summary>
            The range of the function declaration
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.DeclKind">
            <summary>
            The kind of the function declaration.
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Name">
            <summary>
            The name of the function declaration
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.NumParameters">
            <summary>
            The number of parameters of the function declaration
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Parameters">
            <summary>
            The parameters of the function declaration
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Item(Microsoft.Z3.Expr[])">
            <summary>
            Create expression that applies function to arguments.
            </summary>
            <param name="args"></param>
            <returns></returns>
        </member>
        <member name="T:Microsoft.Z3.FuncDecl.Parameter">
            <summary>
            Function declarations can have Parameters associated with them. 
            </summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Parameter.Int">
            <summary>The int value of the parameter.</summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Parameter.Double">
            <summary>The double value of the parameter.</summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Parameter.Symbol">
            <summary>The Symbol value of the parameter.</summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Parameter.Sort">
            <summary>The Sort value of the parameter.</summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Parameter.AST">
            <summary>The AST value of the parameter.</summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Parameter.FuncDecl">
            <summary>The FunctionDeclaration value of the parameter.</summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Parameter.Rational">
            <summary>The rational string value of the parameter.</summary>
        </member>
        <member name="P:Microsoft.Z3.FuncDecl.Parameter.ParameterKind">
            <summary>
            The kind of the parameter.
            </summary>
        </member>
    </members>
</doc>
